# HG changeset patch
# User wenzelm
# Date 1005863146 -3600
# Node ID 6597093b77e70f794c5b33714178d0cf35a9e3eb
# Parent  e3efc5c9f267fde37d395c8a9f6fde14b65edc04
GPLed;

diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Abschannel.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Abschannel_finite.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Action.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Check.ML
--- 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.
 *)
 
  
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Correctness.ML
--- 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)
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Correctness.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Env.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Impl.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Impl_finite.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Lemmas.ML
--- 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 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Lemmas.thy
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Packet.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/ROOT.ML
--- 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;
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Receiver.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Sender.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ABP/Spec.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Modelcheck/ROOT.ML
--- 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.
 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Abschannel.ML
--- 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;
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Abschannel.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Action.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Correctness.ML
--- 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 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Correctness.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Impl.ML
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Impl.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Lemmas.ML
--- 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 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Lemmas.thy
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Multiset.ML
--- 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.
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Multiset.thy
--- 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.
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Packet.ML
--- 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);
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Packet.thy
--- 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 +  
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/ROOT.ML
--- 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;
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Receiver.ML
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Receiver.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Sender.ML
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Sender.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/NTP/Spec.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ROOT.ML
--- 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.
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Action.ML
--- 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 =     \
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Action.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Correctness.ML
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Correctness.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Impl.ML
--- 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 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Impl.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/ROOT.ML
--- 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.
 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/Storage/Spec.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ex/ROOT.ML
--- 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.
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ex/TrivEx.ML
--- 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";
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ex/TrivEx.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ex/TrivEx2.ML
--- 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";
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/ex/TrivEx2.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Abstraction.ML
--- 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";
 	
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- 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.
 *)   
 
 		       
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Asig.ML
--- 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];
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Asig.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Automata.ML
--- 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.
 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Automata.thy
--- 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.
 *)   
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- 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.
 *)  
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- 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.
 *)  
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- 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.
 *) 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- 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.
 *) 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- 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.
 *) 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- 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.
 *) 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Compositionality.ML
--- 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
 *) 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Compositionality.thy
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- 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.
 *)   
 
 (********************************************************************************
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Deadlock.thy
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/IOA.ML
--- 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.
 *)  
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/IOA.thy
--- 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
-
-
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/LiveIOA.ML
--- 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];
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Pred.thy
--- 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 +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- 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";
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- 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  +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Seq.ML
--- 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);
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Seq.thy
--- 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.
 *)  
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Sequence.ML
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Sequence.thy
--- 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 + 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- 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.
-
 *) 
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- 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.
-
 *) 
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Simulations.ML
--- 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.
 *)
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Simulations.thy
--- 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  +
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/TL.ML
--- 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.
 *)   
 
 
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/TL.thy
--- 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
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/TLS.ML
--- 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 *)
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/TLS.thy
--- 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.
 *)   
 
 		       
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Traces.ML
--- 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.
 *)   
diff -r e3efc5c9f267 -r 6597093b77e7 src/HOLCF/IOA/meta_theory/Traces.thy
--- 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.
 *)