Skip to content

Commit 6f7c472

Browse files
committed
update Program.thy
1 parent f2f5196 commit 6f7c472

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

tests/positive/Isabelle/isabelle/Program.thy

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -272,10 +272,12 @@ fun message :: "'MessageType MessagePacket \<Rightarrow> 'MessageType" where
272272
message'"
273273

274274
fun sender :: "'MessageType EnvelopedMessage \<Rightarrow> nat option" where
275-
"sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = sender'"
275+
"sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) =
276+
sender'"
276277

277278
fun packet :: "'MessageType EnvelopedMessage \<Rightarrow> 'MessageType MessagePacket" where
278-
"packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = packet'"
279+
"packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) =
280+
packet'"
279281

280282
fun time :: "'HandleType Timer \<Rightarrow> nat" where
281283
"time (| Timer.time = time', Timer.handle = handle' |) = time'"

0 commit comments

Comments
 (0)