--- a/src/HOLCF/IOA/ABP/Abschannel.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Abschannel.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Abschannel.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The transmission channel
+The transmission channel.
*)
Abschannel = IOA + Action + Lemmas + List +
--- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Abschannels.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The transmission channel -- finite version
+The transmission channel -- finite version.
*)
Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
--- a/src/HOLCF/IOA/ABP/Action.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Action.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Action.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The set of all actions of the system
+The set of all actions of the system.
*)
Action = Packet + Datatype +
--- a/src/HOLCF/IOA/ABP/Check.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Check.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Check.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1994 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The Model Checker
+The Model Checker.
*)
--- a/src/HOLCF/IOA/ABP/Correctness.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,8 +1,7 @@
- (* Title: HOLCF/IOA/ABP/Correctness.ML
+(* Title: HOLCF/IOA/ABP/Correctness.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
-
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
--- a/src/HOLCF/IOA/ABP/Correctness.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Correctness.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The main correctness proof: System_fin implements System
+The main correctness proof: System_fin implements System.
*)
Correctness = IOA + Env + Impl + Impl_finite +
--- a/src/HOLCF/IOA/ABP/Env.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Env.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The environment
+The environment.
*)
Env = IOA + Action +
--- a/src/HOLCF/IOA/ABP/Impl.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Impl.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation
+The implementation.
*)
Impl = Sender + Receiver + Abschannel +
--- a/src/HOLCF/IOA/ABP/Impl_finite.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Impl.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation
+The implementation.
*)
Impl_finite = Sender + Receiver + Abschannel_finite +
--- a/src/HOLCF/IOA/ABP/Lemmas.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,8 +1,7 @@
(* Title: HOLCF/IOA/ABP/Lemmas.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
-
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
(* Logic *)
--- a/src/HOLCF/IOA/ABP/Lemmas.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Lemmas.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Arithmetic lemmas
+Arithmetic lemmas.
*)
Lemmas = NatArith
--- a/src/HOLCF/IOA/ABP/Packet.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Packet.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Packet.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Packets
+Packets.
*)
Packet = NatArith +
--- a/src/HOLCF/IOA/ABP/ROOT.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/ROOT.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,11 +1,10 @@
(* Title: HOL/IOA/ABP/ROOT.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
This is the ROOT file for the Alternating Bit Protocol performed in
-I/O-Automata.
-*)
+I/O-Automata. *)
goals_limit := 1;
--- a/src/HOLCF/IOA/ABP/Receiver.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Receiver.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Receiver.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation: receiver
+The implementation: receiver.
*)
Receiver = List + IOA + Action + Lemmas +
--- a/src/HOLCF/IOA/ABP/Sender.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Sender.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Sender.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation: sender
+The implementation: sender.
*)
Sender = IOA + Action + List + Lemmas +
--- a/src/HOLCF/IOA/ABP/Spec.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ABP/Spec.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Spec.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The specification of reliable transmission
+The specification of reliable transmission.
*)
Spec = List + IOA + Action +
--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,6 +1,7 @@
(* Title: HOLCF/IOA/Modelcheck/ROOT.ML
ID: $Id$
- Author: Olaf Mueller and Tobias Hamberger, TU Muenchen
+ Author: Olaf Müller and Tobias Hamberger, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Modelchecker setup for I/O automata.
*)
--- a/src/HOLCF/IOA/NTP/Abschannel.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Abschannel.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Abschannel.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1994 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Derived rules
+Derived rules.
*)
open Abschannel;
--- a/src/HOLCF/IOA/NTP/Abschannel.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Abschannel.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Abschannel.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1994 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The (faulty) transmission channel (both directions)
+The (faulty) transmission channel (both directions).
*)
Abschannel = IOA + Action +
--- a/src/HOLCF/IOA/NTP/Action.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Action.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Action.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The set of all actions of the system
+The set of all actions of the system.
*)
Action = Packet + Datatype +
--- a/src/HOLCF/IOA/NTP/Correctness.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Correctness.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The main correctness proof: Impl implements Spec
+The main correctness proof: Impl implements Spec.
*)
(* repeated from Traces.ML *)
--- a/src/HOLCF/IOA/NTP/Correctness.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Correctness.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The main correctness proof: Impl implements Spec
+The main correctness proof: Impl implements Spec.
*)
Correctness = Impl + Spec +
--- a/src/HOLCF/IOA/NTP/Impl.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Impl.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation --- Invariants
+The implementation --- Invariants.
*)
--- a/src/HOLCF/IOA/NTP/Impl.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Impl.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation
+The implementation.
*)
Impl = Sender + Receiver + Abschannel +
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,8 +1,7 @@
(* Title: HOL/IOA/NTP/Lemmas.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
(* Logic *)
--- a/src/HOLCF/IOA/NTP/Lemmas.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Lemmas.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Arithmetic lemmas
+Arithmetic lemmas.
*)
Lemmas = NatArith
--- a/src/HOLCF/IOA/NTP/Multiset.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/NTP/Multiset.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Axiomatic multisets.
Should be done as a subtype and moved to a global place.
--- a/src/HOLCF/IOA/NTP/Multiset.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/NTP/Multiset.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Axiomatic multisets.
Should be done as a subtype and moved to a global place.
--- a/src/HOLCF/IOA/NTP/Packet.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Packet.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/IOA/NTP/Packet.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Packets
+Packets.
*)
-
(* Instantiation of a tautology? *)
Goal "!x. x = packet --> hdr(x) = hdr(packet)";
by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
--- a/src/HOLCF/IOA/NTP/Packet.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Packet.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Packet.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Packets
+Packets.
*)
Packet = Multiset +
--- a/src/HOLCF/IOA/NTP/ROOT.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/ROOT.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,10 +1,11 @@
(* Title: HOL/IOA/examples/NTP/ROOT.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-This is the ROOT file for a network transmission protocol (NTP subdirectory),
-performed in the I/O automata formalization by Olaf Mueller.
+This is the ROOT file for a network transmission protocol (NTP
+subdirectory), performed in the I/O automata formalization by Olaf
+Müller.
*)
goals_limit := 1;
--- a/src/HOLCF/IOA/NTP/Receiver.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Receiver.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/NTP/Receiver.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
Goal
--- a/src/HOLCF/IOA/NTP/Receiver.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Receiver.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Receiver.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation: receiver
+The implementation: receiver.
*)
Receiver = List + IOA + Action +
--- a/src/HOLCF/IOA/NTP/Sender.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Sender.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/NTP/Sender.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
Goal
--- a/src/HOLCF/IOA/NTP/Sender.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Sender.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Sender.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation: sender
+The implementation: sender.
*)
Sender = IOA + Action + List +
--- a/src/HOLCF/IOA/NTP/Spec.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Spec.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/NTP/Spec.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The specification of reliable transmission
+The specification of reliable transmission.
*)
Spec = List + IOA + Action +
--- a/src/HOLCF/IOA/ROOT.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ROOT.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/ROOT.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
This is the ROOT file for the formalization of a semantic model of
I/O-Automata. See the README.html file for details.
--- a/src/HOLCF/IOA/Storage/Action.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Action.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Action.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Derived rules for actions
+Derived rules for actions.
*)
Goal "!!x. x = y ==> action_case a b c x = \
--- a/src/HOLCF/IOA/Storage/Action.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Action.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/ABP/Action.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The set of all actions of the system
+The set of all actions of the system.
*)
Action = Main +
--- a/src/HOLCF/IOA/Storage/Correctness.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/example/Correctness.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Correctness Proof
+Correctness Proof.
*)
--- a/src/HOLCF/IOA/Storage/Correctness.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/example/Correctness.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Correctness Proof
+Correctness Proof.
*)
Correctness = SimCorrectness + Spec + Impl +
--- a/src/HOLCF/IOA/Storage/Impl.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Impl.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/example/Sender.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Impl
+Impl.
*)
Goal
--- a/src/HOLCF/IOA/Storage/Impl.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Impl.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/example/Spec.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The implementation of a memory
+The implementation of a memory.
*)
Impl = IOA + Action +
--- a/src/HOLCF/IOA/Storage/ROOT.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/ROOT.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/Storage/ROOT.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1998 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Memory storage case study.
*)
--- a/src/HOLCF/IOA/Storage/Spec.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Spec.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/example/Spec.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The specification of a memory
+The specification of a memory.
*)
Spec = IOA + Action +
--- a/src/HOLCF/IOA/ex/ROOT.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ex/ROOT.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/IOA/ex/ROOT.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
This is the ROOT file for the formalization of a semantic model of
I/O-Automata. See the README.html file for details.
--- a/src/HOLCF/IOA/ex/TrivEx.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/TrivEx.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Trivial Abstraction Example
+Trivial Abstraction Example.
*)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
--- a/src/HOLCF/IOA/ex/TrivEx.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/TrivEx.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Trivial Abstraction Example
+Trivial Abstraction Example.
*)
TrivEx = Abstraction +
--- a/src/HOLCF/IOA/ex/TrivEx2.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx2.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/TrivEx.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Trivial Abstraction Example
+Trivial Abstraction Example.
*)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
--- a/src/HOLCF/IOA/ex/TrivEx2.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/ex/TrivEx2.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/TrivEx.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Trivial Abstraction Example with fairness
+Trivial Abstraction Example with fairness.
*)
TrivEx2 = Abstraction + IOA +
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,13 +1,11 @@
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Abstraction Theory -- tailored for I/O automata
+Abstraction Theory -- tailored for I/O automata.
*)
-
-
section "cex_abs";
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Abstraction Theory -- tailored for I/O automata
+Abstraction Theory -- tailored for I/O automata.
*)
--- a/src/HOLCF/IOA/meta_theory/Asig.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/meta_theory/Asig.ML
ID: $Id$
- Author: Olaf Mueller, Tobias Nipkow & Konrad Slind
- Copyright 1994,1996 TU Muenchen
+ Author: Olaf Müller, Tobias Nipkow & Konrad Slind
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Action signatures
+Action signatures.
*)
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
--- a/src/HOLCF/IOA/meta_theory/Asig.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/IOA/meta_theory/Asig.thy
ID: $Id$
- Author: Olaf Mueller, Tobias Nipkow & Konrad Slind
- Copyright 1994, 1996 TU Muenchen
+ Author: Olaf Müller, Tobias Nipkow & Konrad Slind
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Action signatures
+Action signatures.
*)
Asig = Main +
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Automata.ML
ID: $Id$
Author: Olaf Mueller, Tobias Nipkow, Konrad Slind
- Copyright 1994, 1996 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The I/O automata of Lynch and Tuttle.
*)
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Automata.thy
ID: $Id$
- Author: Olaf M"uller, Konrad Slind, Tobias Nipkow
- Copyright 1995, 1996 TU Muenchen
+ Author: Olaf Müller, Konrad Slind, Tobias Nipkow
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The I/O automata of Lynch and Tuttle in HOLCF.
*)
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality on Execution level.
*)
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality on Execution level.
*)
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/CompoScheds.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality on Schedule level.
*)
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality on Schedule level.
*)
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/CompoTraces.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality on Trace level.
*)
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality on Trace level.
*)
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Compositionality of I/O automata
*)
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Compositionality of I/O automata
+Compositionality of I/O automata.
*)
Compositionality = CompoTraces
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Deadlock.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Deadlock freedom of I/O Automata
+Deadlock freedom of I/O Automata.
*)
(********************************************************************************
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Deadlock.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Deadlock freedom of I/O Automata
+Deadlock freedom of I/O Automata.
*)
Deadlock = RefCorrectness + CompoScheds
--- a/src/HOLCF/IOA/meta_theory/IOA.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/IOA.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/IOA.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996,1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The theory of I/O automata in HOLCF.
*)
--- a/src/HOLCF/IOA/meta_theory/IOA.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,13 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/IOA.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996,1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The theory of I/O automata in HOLCF.
*)
-
-
IOA = SimCorrectness + Compositionality + Deadlock
-
-
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/LiveIOA.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Live I/O Automata
-
+Live I/O Automata.
*)
Delsimps [split_paired_Ex];
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Live I/O automata -- specified by temproal formulas
-
+Live I/O automata -- specified by temproal formulas.
*)
LiveIOA = TLS +
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Pred.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Logical Connectives lifted to predicates.
-
*)
Pred = Main +
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Correctness of Refinement Mappings in HOLCF/IOA
+Correctness of Refinement Mappings in HOLCF/IOA.
*)
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Correctness of Refinement Mappings in HOLCF/IOA
+Correctness of Refinement Mappings in HOLCF/IOA.
*)
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,15 +1,12 @@
(* Title: HOLCF/IOA/meta_theory/RefMappings.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Refinement Mappings in HOLCF/IOA
+Refinement Mappings in HOLCF/IOA.
*)
-
-
-
(* ---------------------------------------------------------------------------- *)
section "transitions and moves";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Refinement Mappings in HOLCF/IOA
+Refinement Mappings in HOLCF/IOA.
*)
RefMappings = Traces +
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,8 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Seq.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
-
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
Addsimps (sfinite.intrs @ seq.rews);
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Seq.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Partial, Finite and Infinite Sequences (lazy lists), modeled as domain.
*)
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Theorems about Sequences over flat domains with lifted elements
-
+Theorems about Sequences over flat domains with lifted elements.
*)
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Sequence.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Sequences over flat domains with lifted elements
-
+Sequences over flat domains with lifted elements.
*)
Sequence = Seq +
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,13 +1,12 @@
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Some properties about (Cut ex), defined as follows:
For every execution ex there is another shorter execution (Cut ex)
that has the same trace as ex, but its schedule ends with an external action.
-
*)
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,13 +1,12 @@
(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Some properties about (Cut ex), defined as follows:
For every execution ex there is another shorter execution (Cut ex)
that has the same trace as ex, but its schedule ends with an external action.
-
*)
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Correctness of Simulations in HOLCF/IOA
+Correctness of Simulations in HOLCF/IOA.
*)
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Correctness of Simulations in HOLCF/IOA
+Correctness of Simulations in HOLCF/IOA.
*)
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Simulations.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Simulations in HOLCF/IOA
+Simulations in HOLCF/IOA.
*)
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Simulations.thy
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Simulations in HOLCF/IOA
+Simulations in HOLCF/IOA.
*)
Simulations = RefCorrectness +
--- a/src/HOLCF/IOA/meta_theory/TL.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/TL.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Temporal Logic
+Temporal Logic.
*)
--- a/src/HOLCF/IOA/meta_theory/TL.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,14 +1,11 @@
(* Title: HOLCF/IOA/meta_theory/TLS.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
-
-A General Temporal Logic
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+A General Temporal Logic.
*)
-
-
-
+
TL = Pred + Sequence +
default term
--- a/src/HOLCF/IOA/meta_theory/TLS.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/TLS.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Temporal Logic of Steps -- tailored for I/O automata
+Temporal Logic of Steps -- tailored for I/O automata.
*)
(* global changes to simpset() and claset(), repeated from Traces.ML *)
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/TLS.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1997 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Temporal Logic of Steps -- tailored for I/O automata
+Temporal Logic of Steps -- tailored for I/O automata.
*)
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Traces.ML
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Theorems about Executions and Traces of I/O automata in HOLCF.
*)
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Thu Nov 15 23:25:01 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Thu Nov 15 23:25:46 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/IOA/meta_theory/Traces.thy
ID: $Id$
- Author: Olaf M"uller
- Copyright 1996 TU Muenchen
+ Author: Olaf Müller
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Executions and Traces of I/O automata in HOLCF.
*)