update Program.thy

anoma · Dec 1, 2024 · 5da7a09 · 5da7a09
1 parent 41eef7a
commit 5da7a09
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
@@ -272,10 +272,12 @@ fun message :: "'MessageType MessagePacket \<Rightarrow> 'MessageType" where
     message'"
 
 fun sender :: "'MessageType EnvelopedMessage \<Rightarrow> nat option" where
-  "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = sender'"
+  "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) =
+    sender'"
 
 fun packet :: "'MessageType EnvelopedMessage \<Rightarrow> 'MessageType MessagePacket" where
-  "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = packet'"
+  "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) =
+    packet'"
 
 fun time :: "'HandleType Timer \<Rightarrow> nat" where
   "time (| Timer.time = time', Timer.handle = handle' |) = time'"