From 5da7a09b1b028a6bbce2ef60326aabf711aed4ac Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Sun, 1 Dec 2024 13:45:01 +0100 Subject: [PATCH] update Program.thy --- tests/positive/Isabelle/isabelle/Program.thy | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 59988ae8d7..f19fe19e64 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -272,10 +272,12 @@ fun message :: "'MessageType MessagePacket \ 'MessageType" where message'" fun sender :: "'MessageType EnvelopedMessage \ nat option" where - "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = sender'" + "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = + sender'" fun packet :: "'MessageType EnvelopedMessage \ 'MessageType MessagePacket" where - "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = packet'" + "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = + packet'" fun time :: "'HandleType Timer \ nat" where "time (| Timer.time = time', Timer.handle = handle' |) = time'"