GPLed;
authorwenzelm
Thu Nov 15 23:25:46 2001 +0100 (2001-11-15 ago)
changeset 122186597093b77e7
parent 12217 e3efc5c9f267
child 12219 ae54aa9f6d08
GPLed;
src/HOLCF/IOA/ABP/Abschannel.thy
src/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOLCF/IOA/ABP/Action.thy
src/HOLCF/IOA/ABP/Check.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Correctness.thy
src/HOLCF/IOA/ABP/Env.thy
src/HOLCF/IOA/ABP/Impl.thy
src/HOLCF/IOA/ABP/Impl_finite.thy
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/ABP/Lemmas.thy
src/HOLCF/IOA/ABP/Packet.thy
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/ABP/Receiver.thy
src/HOLCF/IOA/ABP/Sender.thy
src/HOLCF/IOA/ABP/Spec.thy
src/HOLCF/IOA/Modelcheck/ROOT.ML
src/HOLCF/IOA/NTP/Abschannel.ML
src/HOLCF/IOA/NTP/Abschannel.thy
src/HOLCF/IOA/NTP/Action.thy
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/NTP/Correctness.thy
src/HOLCF/IOA/NTP/Impl.ML
src/HOLCF/IOA/NTP/Impl.thy
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/NTP/Lemmas.thy
src/HOLCF/IOA/NTP/Multiset.ML
src/HOLCF/IOA/NTP/Multiset.thy
src/HOLCF/IOA/NTP/Packet.ML
src/HOLCF/IOA/NTP/Packet.thy
src/HOLCF/IOA/NTP/ROOT.ML
src/HOLCF/IOA/NTP/Receiver.ML
src/HOLCF/IOA/NTP/Receiver.thy
src/HOLCF/IOA/NTP/Sender.ML
src/HOLCF/IOA/NTP/Sender.thy
src/HOLCF/IOA/NTP/Spec.thy
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/Storage/Action.ML
src/HOLCF/IOA/Storage/Action.thy
src/HOLCF/IOA/Storage/Correctness.ML
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/Storage/Impl.ML
src/HOLCF/IOA/Storage/Impl.thy
src/HOLCF/IOA/Storage/ROOT.ML
src/HOLCF/IOA/Storage/Spec.thy
src/HOLCF/IOA/ex/ROOT.ML
src/HOLCF/IOA/ex/TrivEx.ML
src/HOLCF/IOA/ex/TrivEx.thy
src/HOLCF/IOA/ex/TrivEx2.ML
src/HOLCF/IOA/ex/TrivEx2.thy
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Asig.ML
src/HOLCF/IOA/meta_theory/Asig.thy
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOLCF/IOA/meta_theory/IOA.ML
src/HOLCF/IOA/meta_theory/IOA.thy
src/HOLCF/IOA/meta_theory/LiveIOA.ML
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOLCF/IOA/meta_theory/Simulations.ML
src/HOLCF/IOA/meta_theory/Simulations.thy
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/IOA/meta_theory/Traces.thy
     1.1 --- a/src/HOLCF/IOA/ABP/Abschannel.thy	Thu Nov 15 23:25:01 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy	Thu Nov 15 23:25:46 2001 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  Title:      HOLCF/IOA/ABP/Abschannel.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Olaf Mueller
     1.7 -    Copyright   1995  TU Muenchen
     1.8 +    Author:     Olaf Müller
     1.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11 -The transmission channel 
    1.12 +The transmission channel.
    1.13  *)
    1.14  
    1.15  Abschannel = IOA + Action + Lemmas + List +
     2.1 --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Nov 15 23:25:01 2001 +0100
     2.2 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Nov 15 23:25:46 2001 +0100
     2.3 @@ -1,9 +1,9 @@
     2.4  (*  Title:      HOLCF/IOA/ABP/Abschannels.thy
     2.5      ID:         $Id$
     2.6 -    Author:     Olaf Mueller
     2.7 -    Copyright   1995  TU Muenchen
     2.8 +    Author:     Olaf Müller
     2.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    2.10  
    2.11 -The transmission channel -- finite version
    2.12 +The transmission channel -- finite version.
    2.13  *)
    2.14  
    2.15  Abschannel_finite = Abschannel+ IOA + Action + Lemmas + List +
     3.1 --- a/src/HOLCF/IOA/ABP/Action.thy	Thu Nov 15 23:25:01 2001 +0100
     3.2 +++ b/src/HOLCF/IOA/ABP/Action.thy	Thu Nov 15 23:25:46 2001 +0100
     3.3 @@ -1,9 +1,9 @@
     3.4  (*  Title:      HOLCF/IOA/ABP/Action.thy
     3.5      ID:         $Id$
     3.6 -    Author:     Olaf Mueller
     3.7 -    Copyright   1995  TU Muenchen
     3.8 +    Author:     Olaf Müller
     3.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    3.10  
    3.11 -The set of all actions of the system
    3.12 +The set of all actions of the system.
    3.13  *)
    3.14  
    3.15  Action = Packet + Datatype +
     4.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Thu Nov 15 23:25:01 2001 +0100
     4.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Thu Nov 15 23:25:46 2001 +0100
     4.3 @@ -1,9 +1,9 @@
     4.4  (*  Title:      HOLCF/IOA/ABP/Check.ML
     4.5      ID:         $Id$
     4.6 -    Author:     Olaf Mueller
     4.7 -    Copyright   1994  TU Muenchen
     4.8 +    Author:     Olaf Müller
     4.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    4.10  
    4.11 -The Model Checker
    4.12 +The Model Checker.
    4.13  *)
    4.14  
    4.15   
     5.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Nov 15 23:25:01 2001 +0100
     5.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Thu Nov 15 23:25:46 2001 +0100
     5.3 @@ -1,8 +1,7 @@
     5.4 - (*  Title:      HOLCF/IOA/ABP/Correctness.ML
     5.5 +(*  Title:      HOLCF/IOA/ABP/Correctness.ML
     5.6      ID:         $Id$
     5.7 -    Author:     Olaf Mueller
     5.8 -    Copyright   1995  TU Muenchen
     5.9 -
    5.10 +    Author:     Olaf Müller
    5.11 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    5.12  *)
    5.13  
    5.14  
     6.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Thu Nov 15 23:25:01 2001 +0100
     6.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Thu Nov 15 23:25:46 2001 +0100
     6.3 @@ -1,9 +1,9 @@
     6.4  (*  Title:      HOLCF/IOA/ABP/Correctness.thy
     6.5      ID:         $Id$
     6.6 -    Author:     Olaf Mueller
     6.7 -    Copyright   1995  TU Muenchen
     6.8 +    Author:     Olaf Müller
     6.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    6.10  
    6.11 -The main correctness proof: System_fin implements System
    6.12 +The main correctness proof: System_fin implements System.
    6.13  *)
    6.14  
    6.15  Correctness = IOA + Env + Impl + Impl_finite + 
     7.1 --- a/src/HOLCF/IOA/ABP/Env.thy	Thu Nov 15 23:25:01 2001 +0100
     7.2 +++ b/src/HOLCF/IOA/ABP/Env.thy	Thu Nov 15 23:25:46 2001 +0100
     7.3 @@ -1,9 +1,9 @@
     7.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
     7.5      ID:         $Id$
     7.6 -    Author:     Olaf Mueller
     7.7 -    Copyright   1995  TU Muenchen
     7.8 +    Author:     Olaf Müller
     7.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    7.10  
    7.11 -The environment
    7.12 +The environment.
    7.13  *)
    7.14  
    7.15  Env = IOA + Action +
     8.1 --- a/src/HOLCF/IOA/ABP/Impl.thy	Thu Nov 15 23:25:01 2001 +0100
     8.2 +++ b/src/HOLCF/IOA/ABP/Impl.thy	Thu Nov 15 23:25:46 2001 +0100
     8.3 @@ -1,9 +1,9 @@
     8.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
     8.5      ID:         $Id$
     8.6 -    Author:     Olaf Mueller
     8.7 -    Copyright   1995  TU Muenchen
     8.8 +    Author:     Olaf Müller
     8.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    8.10  
    8.11 -The implementation
    8.12 +The implementation.
    8.13  *)
    8.14  
    8.15  Impl = Sender + Receiver +  Abschannel +
     9.1 --- a/src/HOLCF/IOA/ABP/Impl_finite.thy	Thu Nov 15 23:25:01 2001 +0100
     9.2 +++ b/src/HOLCF/IOA/ABP/Impl_finite.thy	Thu Nov 15 23:25:46 2001 +0100
     9.3 @@ -1,9 +1,9 @@
     9.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
     9.5      ID:         $Id$
     9.6 -    Author:     Olaf Mueller
     9.7 -    Copyright   1995  TU Muenchen
     9.8 +    Author:     Olaf Müller
     9.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    9.10  
    9.11 -The implementation
    9.12 +The implementation.
    9.13  *)
    9.14  
    9.15  Impl_finite = Sender + Receiver +  Abschannel_finite +
    10.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Nov 15 23:25:01 2001 +0100
    10.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Nov 15 23:25:46 2001 +0100
    10.3 @@ -1,8 +1,7 @@
    10.4  (*  Title:      HOLCF/IOA/ABP/Lemmas.ML
    10.5      ID:         $Id$
    10.6 -    Author:     Olaf Mueller
    10.7 -    Copyright   1995  TU Muenchen
    10.8 -
    10.9 +    Author:     Olaf Müller
   10.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   10.11  *)
   10.12  
   10.13  (* Logic *)
    11.1 --- a/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Nov 15 23:25:01 2001 +0100
    11.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Nov 15 23:25:46 2001 +0100
    11.3 @@ -1,9 +1,9 @@
    11.4  (*  Title:      HOLCF/IOA/ABP/Lemmas.thy
    11.5      ID:         $Id$
    11.6 -    Author:     Olaf Mueller
    11.7 -    Copyright   1995  TU Muenchen
    11.8 +    Author:     Olaf Müller
    11.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   11.10  
   11.11 -Arithmetic lemmas
   11.12 +Arithmetic lemmas.
   11.13  *)
   11.14  
   11.15  Lemmas = NatArith
    12.1 --- a/src/HOLCF/IOA/ABP/Packet.thy	Thu Nov 15 23:25:01 2001 +0100
    12.2 +++ b/src/HOLCF/IOA/ABP/Packet.thy	Thu Nov 15 23:25:46 2001 +0100
    12.3 @@ -1,9 +1,9 @@
    12.4  (*  Title:      HOLCF/IOA/ABP/Packet.thy
    12.5      ID:         $Id$
    12.6 -    Author:     Olaf Mueller
    12.7 -    Copyright   1995  TU Muenchen
    12.8 +    Author:     Olaf Müller
    12.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   12.10  
   12.11 -Packets
   12.12 +Packets.
   12.13  *)
   12.14  
   12.15  Packet = NatArith +
    13.1 --- a/src/HOLCF/IOA/ABP/ROOT.ML	Thu Nov 15 23:25:01 2001 +0100
    13.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Thu Nov 15 23:25:46 2001 +0100
    13.3 @@ -1,11 +1,10 @@
    13.4  (*  Title:      HOL/IOA/ABP/ROOT.ML
    13.5      ID:         $Id$
    13.6 -    Author:     Olaf Mueller
    13.7 -    Copyright   1995  TU Muenchen
    13.8 +    Author:     Olaf Müller
    13.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   13.10  
   13.11  This is the ROOT file for the Alternating Bit Protocol performed in
   13.12 -I/O-Automata.
   13.13 -*)
   13.14 +I/O-Automata.  *)
   13.15  
   13.16  goals_limit := 1;
   13.17  
    14.1 --- a/src/HOLCF/IOA/ABP/Receiver.thy	Thu Nov 15 23:25:01 2001 +0100
    14.2 +++ b/src/HOLCF/IOA/ABP/Receiver.thy	Thu Nov 15 23:25:46 2001 +0100
    14.3 @@ -1,9 +1,9 @@
    14.4  (*  Title:      HOLCF/IOA/ABP/Receiver.thy
    14.5      ID:         $Id$
    14.6 -    Author:     Olaf Mueller
    14.7 -    Copyright   1995  TU Muenchen
    14.8 +    Author:     Olaf Müller
    14.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   14.10  
   14.11 -The implementation: receiver
   14.12 +The implementation: receiver.
   14.13  *)
   14.14  
   14.15  Receiver = List + IOA + Action + Lemmas +
    15.1 --- a/src/HOLCF/IOA/ABP/Sender.thy	Thu Nov 15 23:25:01 2001 +0100
    15.2 +++ b/src/HOLCF/IOA/ABP/Sender.thy	Thu Nov 15 23:25:46 2001 +0100
    15.3 @@ -1,9 +1,9 @@
    15.4  (*  Title:      HOLCF/IOA/ABP/Sender.thy
    15.5      ID:         $Id$
    15.6 -    Author:     Olaf Mueller
    15.7 -    Copyright   1995  TU Muenchen
    15.8 +    Author:     Olaf Müller
    15.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   15.10  
   15.11 -The implementation: sender
   15.12 +The implementation: sender.
   15.13  *)
   15.14  
   15.15  Sender = IOA + Action + List + Lemmas +
    16.1 --- a/src/HOLCF/IOA/ABP/Spec.thy	Thu Nov 15 23:25:01 2001 +0100
    16.2 +++ b/src/HOLCF/IOA/ABP/Spec.thy	Thu Nov 15 23:25:46 2001 +0100
    16.3 @@ -1,9 +1,9 @@
    16.4  (*  Title:      HOLCF/IOA/ABP/Spec.thy
    16.5      ID:         $Id$
    16.6 -    Author:     Olaf Mueller
    16.7 -    Copyright   1995  TU Muenchen
    16.8 +    Author:     Olaf Müller
    16.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   16.10  
   16.11 -The specification of reliable transmission
   16.12 +The specification of reliable transmission.
   16.13  *)
   16.14  
   16.15  Spec = List + IOA + Action +
    17.1 --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Nov 15 23:25:01 2001 +0100
    17.2 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Thu Nov 15 23:25:46 2001 +0100
    17.3 @@ -1,6 +1,7 @@
    17.4  (*  Title:      HOLCF/IOA/Modelcheck/ROOT.ML
    17.5      ID:         $Id$
    17.6 -    Author:     Olaf Mueller and Tobias Hamberger, TU Muenchen
    17.7 +    Author:     Olaf Müller and Tobias Hamberger, TU Muenchen
    17.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    17.9  
   17.10  Modelchecker setup for I/O automata.
   17.11  *)
    18.1 --- a/src/HOLCF/IOA/NTP/Abschannel.ML	Thu Nov 15 23:25:01 2001 +0100
    18.2 +++ b/src/HOLCF/IOA/NTP/Abschannel.ML	Thu Nov 15 23:25:46 2001 +0100
    18.3 @@ -1,9 +1,9 @@
    18.4  (*  Title:      HOL/IOA/NTP/Abschannel.ML
    18.5      ID:         $Id$
    18.6 -    Author:     Olaf Mueller
    18.7 -    Copyright   1994  TU Muenchen
    18.8 +    Author:     Olaf Müller
    18.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   18.10  
   18.11 -Derived rules
   18.12 +Derived rules.
   18.13  *)
   18.14  
   18.15  open Abschannel;
    19.1 --- a/src/HOLCF/IOA/NTP/Abschannel.thy	Thu Nov 15 23:25:01 2001 +0100
    19.2 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy	Thu Nov 15 23:25:46 2001 +0100
    19.3 @@ -1,9 +1,9 @@
    19.4  (*  Title:      HOL/IOA/NTP/Abschannel.thy
    19.5      ID:         $Id$
    19.6 -    Author:     Olaf Mueller
    19.7 -    Copyright   1994  TU Muenchen
    19.8 +    Author:     Olaf Müller
    19.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   19.10  
   19.11 -The (faulty) transmission channel (both directions)
   19.12 +The (faulty) transmission channel (both directions).
   19.13  *)
   19.14  
   19.15  Abschannel = IOA + Action + 
    20.1 --- a/src/HOLCF/IOA/NTP/Action.thy	Thu Nov 15 23:25:01 2001 +0100
    20.2 +++ b/src/HOLCF/IOA/NTP/Action.thy	Thu Nov 15 23:25:46 2001 +0100
    20.3 @@ -1,9 +1,9 @@
    20.4  (*  Title:      HOL/IOA/NTP/Action.thy
    20.5      ID:         $Id$
    20.6      Author:     Tobias Nipkow & Konrad Slind
    20.7 -    Copyright   1994  TU Muenchen
    20.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    20.9  
   20.10 -The set of all actions of the system
   20.11 +The set of all actions of the system.
   20.12  *)
   20.13  
   20.14  Action = Packet + Datatype +
    21.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Thu Nov 15 23:25:01 2001 +0100
    21.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Thu Nov 15 23:25:46 2001 +0100
    21.3 @@ -1,9 +1,9 @@
    21.4  (*  Title:      HOL/IOA/NTP/Correctness.ML
    21.5      ID:         $Id$
    21.6      Author:     Tobias Nipkow & Konrad Slind
    21.7 -    Copyright   1994  TU Muenchen
    21.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    21.9  
   21.10 -The main correctness proof: Impl implements Spec
   21.11 +The main correctness proof: Impl implements Spec.
   21.12  *)
   21.13  
   21.14  (* repeated from Traces.ML *)
    22.1 --- a/src/HOLCF/IOA/NTP/Correctness.thy	Thu Nov 15 23:25:01 2001 +0100
    22.2 +++ b/src/HOLCF/IOA/NTP/Correctness.thy	Thu Nov 15 23:25:46 2001 +0100
    22.3 @@ -1,9 +1,9 @@
    22.4  (*  Title:      HOL/IOA/NTP/Correctness.thy
    22.5      ID:         $Id$
    22.6      Author:     Tobias Nipkow & Konrad Slind
    22.7 -    Copyright   1994  TU Muenchen
    22.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    22.9  
   22.10 -The main correctness proof: Impl implements Spec
   22.11 +The main correctness proof: Impl implements Spec.
   22.12  *)
   22.13  
   22.14  Correctness = Impl + Spec +
    23.1 --- a/src/HOLCF/IOA/NTP/Impl.ML	Thu Nov 15 23:25:01 2001 +0100
    23.2 +++ b/src/HOLCF/IOA/NTP/Impl.ML	Thu Nov 15 23:25:46 2001 +0100
    23.3 @@ -1,9 +1,9 @@
    23.4  (*  Title:      HOL/IOA/NTP/Impl.ML
    23.5      ID:         $Id$
    23.6      Author:     Tobias Nipkow & Konrad Slind
    23.7 -    Copyright   1994  TU Muenchen
    23.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    23.9  
   23.10 -The implementation --- Invariants
   23.11 +The implementation --- Invariants.
   23.12  *)
   23.13  
   23.14  
    24.1 --- a/src/HOLCF/IOA/NTP/Impl.thy	Thu Nov 15 23:25:01 2001 +0100
    24.2 +++ b/src/HOLCF/IOA/NTP/Impl.thy	Thu Nov 15 23:25:46 2001 +0100
    24.3 @@ -1,9 +1,9 @@
    24.4  (*  Title:      HOL/IOA/NTP/Impl.thy
    24.5      ID:         $Id$
    24.6      Author:     Tobias Nipkow & Konrad Slind
    24.7 -    Copyright   1994  TU Muenchen
    24.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    24.9  
   24.10 -The implementation
   24.11 +The implementation.
   24.12  *)
   24.13  
   24.14  Impl = Sender + Receiver + Abschannel +
    25.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Thu Nov 15 23:25:01 2001 +0100
    25.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Thu Nov 15 23:25:46 2001 +0100
    25.3 @@ -1,8 +1,7 @@
    25.4  (*  Title:      HOL/IOA/NTP/Lemmas.ML
    25.5      ID:         $Id$
    25.6      Author:     Tobias Nipkow & Konrad Slind
    25.7 -    Copyright   1994  TU Muenchen
    25.8 -
    25.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   25.10  *)
   25.11  
   25.12  (* Logic *)
    26.1 --- a/src/HOLCF/IOA/NTP/Lemmas.thy	Thu Nov 15 23:25:01 2001 +0100
    26.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.thy	Thu Nov 15 23:25:46 2001 +0100
    26.3 @@ -1,9 +1,9 @@
    26.4  (*  Title:      HOL/IOA/NTP/Lemmas.thy
    26.5      ID:         $Id$
    26.6      Author:     Tobias Nipkow & Konrad Slind
    26.7 -    Copyright   1994  TU Muenchen
    26.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    26.9  
   26.10 -Arithmetic lemmas
   26.11 +Arithmetic lemmas.
   26.12  *)
   26.13  
   26.14  Lemmas = NatArith
    27.1 --- a/src/HOLCF/IOA/NTP/Multiset.ML	Thu Nov 15 23:25:01 2001 +0100
    27.2 +++ b/src/HOLCF/IOA/NTP/Multiset.ML	Thu Nov 15 23:25:46 2001 +0100
    27.3 @@ -1,7 +1,7 @@
    27.4  (*  Title:      HOL/IOA/NTP/Multiset.ML
    27.5      ID:         $Id$
    27.6      Author:     Tobias Nipkow & Konrad Slind
    27.7 -    Copyright   1994  TU Muenchen
    27.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    27.9  
   27.10  Axiomatic multisets.
   27.11  Should be done as a subtype and moved to a global place.
    28.1 --- a/src/HOLCF/IOA/NTP/Multiset.thy	Thu Nov 15 23:25:01 2001 +0100
    28.2 +++ b/src/HOLCF/IOA/NTP/Multiset.thy	Thu Nov 15 23:25:46 2001 +0100
    28.3 @@ -1,7 +1,7 @@
    28.4  (*  Title:      HOL/IOA/NTP/Multiset.thy
    28.5      ID:         $Id$
    28.6      Author:     Tobias Nipkow & Konrad Slind
    28.7 -    Copyright   1994  TU Muenchen
    28.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    28.9  
   28.10  Axiomatic multisets.
   28.11  Should be done as a subtype and moved to a global place.
    29.1 --- a/src/HOLCF/IOA/NTP/Packet.ML	Thu Nov 15 23:25:01 2001 +0100
    29.2 +++ b/src/HOLCF/IOA/NTP/Packet.ML	Thu Nov 15 23:25:46 2001 +0100
    29.3 @@ -1,12 +1,11 @@
    29.4  (*  Title:      HOL/IOA/NTP/Packet.ML
    29.5      ID:         $Id$
    29.6      Author:     Tobias Nipkow & Konrad Slind
    29.7 -    Copyright   1994  TU Muenchen
    29.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    29.9  
   29.10 -Packets
   29.11 +Packets.
   29.12  *)
   29.13  
   29.14 -
   29.15  (* Instantiation of a tautology? *)
   29.16  Goal "!x. x = packet --> hdr(x) = hdr(packet)";
   29.17   by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
    30.1 --- a/src/HOLCF/IOA/NTP/Packet.thy	Thu Nov 15 23:25:01 2001 +0100
    30.2 +++ b/src/HOLCF/IOA/NTP/Packet.thy	Thu Nov 15 23:25:46 2001 +0100
    30.3 @@ -1,9 +1,9 @@
    30.4  (*  Title:      HOL/IOA/NTP/Packet.thy
    30.5      ID:         $Id$
    30.6      Author:     Tobias Nipkow & Konrad Slind
    30.7 -    Copyright   1994  TU Muenchen
    30.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    30.9  
   30.10 -Packets
   30.11 +Packets.
   30.12  *)
   30.13  
   30.14  Packet = Multiset +  
    31.1 --- a/src/HOLCF/IOA/NTP/ROOT.ML	Thu Nov 15 23:25:01 2001 +0100
    31.2 +++ b/src/HOLCF/IOA/NTP/ROOT.ML	Thu Nov 15 23:25:46 2001 +0100
    31.3 @@ -1,10 +1,11 @@
    31.4  (*  Title:      HOL/IOA/examples/NTP/ROOT.ML
    31.5      ID:         $Id$
    31.6      Author:     Tobias Nipkow & Konrad Slind
    31.7 -    Copyright   1994  TU Muenchen
    31.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    31.9  
   31.10 -This is the ROOT file for a network transmission protocol (NTP subdirectory),
   31.11 -performed in the I/O automata formalization by Olaf Mueller. 
   31.12 +This is the ROOT file for a network transmission protocol (NTP
   31.13 +subdirectory), performed in the I/O automata formalization by Olaf
   31.14 +Müller.
   31.15  *)
   31.16  
   31.17  goals_limit := 1;
    32.1 --- a/src/HOLCF/IOA/NTP/Receiver.ML	Thu Nov 15 23:25:01 2001 +0100
    32.2 +++ b/src/HOLCF/IOA/NTP/Receiver.ML	Thu Nov 15 23:25:46 2001 +0100
    32.3 @@ -1,7 +1,7 @@
    32.4  (*  Title:      HOL/IOA/NTP/Receiver.ML
    32.5      ID:         $Id$
    32.6      Author:     Tobias Nipkow & Konrad Slind
    32.7 -    Copyright   1994  TU Muenchen
    32.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    32.9  *)
   32.10  
   32.11  Goal
    33.1 --- a/src/HOLCF/IOA/NTP/Receiver.thy	Thu Nov 15 23:25:01 2001 +0100
    33.2 +++ b/src/HOLCF/IOA/NTP/Receiver.thy	Thu Nov 15 23:25:46 2001 +0100
    33.3 @@ -1,9 +1,9 @@
    33.4  (*  Title:      HOL/IOA/NTP/Receiver.thy
    33.5      ID:         $Id$
    33.6      Author:     Tobias Nipkow & Konrad Slind
    33.7 -    Copyright   1994  TU Muenchen
    33.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    33.9  
   33.10 -The implementation: receiver
   33.11 +The implementation: receiver.
   33.12  *)
   33.13  
   33.14  Receiver = List + IOA + Action + 
    34.1 --- a/src/HOLCF/IOA/NTP/Sender.ML	Thu Nov 15 23:25:01 2001 +0100
    34.2 +++ b/src/HOLCF/IOA/NTP/Sender.ML	Thu Nov 15 23:25:46 2001 +0100
    34.3 @@ -1,7 +1,7 @@
    34.4  (*  Title:      HOL/IOA/NTP/Sender.ML
    34.5      ID:         $Id$
    34.6      Author:     Tobias Nipkow & Konrad Slind
    34.7 -    Copyright   1994  TU Muenchen
    34.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    34.9  *)
   34.10  
   34.11  Goal
    35.1 --- a/src/HOLCF/IOA/NTP/Sender.thy	Thu Nov 15 23:25:01 2001 +0100
    35.2 +++ b/src/HOLCF/IOA/NTP/Sender.thy	Thu Nov 15 23:25:46 2001 +0100
    35.3 @@ -1,9 +1,9 @@
    35.4  (*  Title:      HOL/IOA/NTP/Sender.thy
    35.5      ID:         $Id$
    35.6      Author:     Tobias Nipkow & Konrad Slind
    35.7 -    Copyright   1994  TU Muenchen
    35.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    35.9  
   35.10 -The implementation: sender
   35.11 +The implementation: sender.
   35.12  *)
   35.13  
   35.14  Sender = IOA + Action + List +
    36.1 --- a/src/HOLCF/IOA/NTP/Spec.thy	Thu Nov 15 23:25:01 2001 +0100
    36.2 +++ b/src/HOLCF/IOA/NTP/Spec.thy	Thu Nov 15 23:25:46 2001 +0100
    36.3 @@ -1,9 +1,9 @@
    36.4  (*  Title:      HOL/IOA/NTP/Spec.thy
    36.5      ID:         $Id$
    36.6      Author:     Tobias Nipkow & Konrad Slind
    36.7 -    Copyright   1994  TU Muenchen
    36.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    36.9  
   36.10 -The specification of reliable transmission
   36.11 +The specification of reliable transmission.
   36.12  *)
   36.13  
   36.14  Spec = List + IOA + Action +
    37.1 --- a/src/HOLCF/IOA/ROOT.ML	Thu Nov 15 23:25:01 2001 +0100
    37.2 +++ b/src/HOLCF/IOA/ROOT.ML	Thu Nov 15 23:25:46 2001 +0100
    37.3 @@ -1,7 +1,7 @@
    37.4  (*  Title:      HOL/IOA/ROOT.ML
    37.5      ID:         $Id$
    37.6 -    Author:     Olaf Mueller
    37.7 -    Copyright   1997  TU Muenchen
    37.8 +    Author:     Olaf Müller
    37.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   37.10  
   37.11  This is the ROOT file for the formalization of a semantic model of
   37.12  I/O-Automata.  See the README.html file for details.
    38.1 --- a/src/HOLCF/IOA/Storage/Action.ML	Thu Nov 15 23:25:01 2001 +0100
    38.2 +++ b/src/HOLCF/IOA/Storage/Action.ML	Thu Nov 15 23:25:46 2001 +0100
    38.3 @@ -1,9 +1,9 @@
    38.4  (*  Title:      HOLCF/IOA/ABP/Action.ML
    38.5      ID:         $Id$
    38.6 -    Author:     Olaf Mueller
    38.7 -    Copyright   1997  TU Muenchen
    38.8 +    Author:     Olaf Müller
    38.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   38.10  
   38.11 -Derived rules for actions
   38.12 +Derived rules for actions.
   38.13  *)
   38.14  
   38.15  Goal "!!x. x = y ==> action_case a b c x =     \
    39.1 --- a/src/HOLCF/IOA/Storage/Action.thy	Thu Nov 15 23:25:01 2001 +0100
    39.2 +++ b/src/HOLCF/IOA/Storage/Action.thy	Thu Nov 15 23:25:46 2001 +0100
    39.3 @@ -1,9 +1,9 @@
    39.4  (*  Title:      HOLCF/IOA/ABP/Action.thy
    39.5      ID:         $Id$
    39.6 -    Author:     Olaf Mueller
    39.7 -    Copyright   1997  TU Muenchen
    39.8 +    Author:     Olaf Müller
    39.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   39.10  
   39.11 -The set of all actions of the system
   39.12 +The set of all actions of the system.
   39.13  *)
   39.14  
   39.15  Action =  Main +
    40.1 --- a/src/HOLCF/IOA/Storage/Correctness.ML	Thu Nov 15 23:25:01 2001 +0100
    40.2 +++ b/src/HOLCF/IOA/Storage/Correctness.ML	Thu Nov 15 23:25:46 2001 +0100
    40.3 @@ -1,9 +1,9 @@
    40.4  (*  Title:      HOL/IOA/example/Correctness.ML
    40.5      ID:         $Id$
    40.6 -    Author:     Olaf Mueller
    40.7 -    Copyright   1997  TU Muenchen
    40.8 +    Author:     Olaf Müller
    40.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   40.10  
   40.11 -Correctness Proof
   40.12 +Correctness Proof.
   40.13  *)
   40.14  
   40.15  
    41.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy	Thu Nov 15 23:25:01 2001 +0100
    41.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Thu Nov 15 23:25:46 2001 +0100
    41.3 @@ -1,9 +1,9 @@
    41.4  (*  Title:      HOL/IOA/example/Correctness.thy
    41.5      ID:         $Id$
    41.6 -    Author:     Olaf Mueller
    41.7 -    Copyright   1997  TU Muenchen
    41.8 +    Author:     Olaf Müller
    41.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   41.10  
   41.11 -Correctness Proof
   41.12 +Correctness Proof.
   41.13  *)
   41.14  
   41.15  Correctness = SimCorrectness + Spec + Impl + 
    42.1 --- a/src/HOLCF/IOA/Storage/Impl.ML	Thu Nov 15 23:25:01 2001 +0100
    42.2 +++ b/src/HOLCF/IOA/Storage/Impl.ML	Thu Nov 15 23:25:46 2001 +0100
    42.3 @@ -1,9 +1,9 @@
    42.4  (*  Title:      HOL/IOA/example/Sender.thy
    42.5      ID:         $Id$
    42.6 -    Author:     Olaf Mueller
    42.7 -    Copyright   1997  TU Muenchen
    42.8 +    Author:     Olaf Müller
    42.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   42.10  
   42.11 -Impl
   42.12 +Impl.
   42.13  *)
   42.14   
   42.15  Goal 
    43.1 --- a/src/HOLCF/IOA/Storage/Impl.thy	Thu Nov 15 23:25:01 2001 +0100
    43.2 +++ b/src/HOLCF/IOA/Storage/Impl.thy	Thu Nov 15 23:25:46 2001 +0100
    43.3 @@ -1,9 +1,9 @@
    43.4  (*  Title:      HOL/IOA/example/Spec.thy
    43.5      ID:         $Id$
    43.6 -    Author:     Olaf Mueller
    43.7 -    Copyright   1997  TU Muenchen
    43.8 +    Author:     Olaf Müller
    43.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   43.10  
   43.11 -The implementation of a memory
   43.12 +The implementation of a memory.
   43.13  *)
   43.14  
   43.15  Impl = IOA + Action +
    44.1 --- a/src/HOLCF/IOA/Storage/ROOT.ML	Thu Nov 15 23:25:01 2001 +0100
    44.2 +++ b/src/HOLCF/IOA/Storage/ROOT.ML	Thu Nov 15 23:25:46 2001 +0100
    44.3 @@ -1,7 +1,7 @@
    44.4  (*  Title:      HOL/IOA/Storage/ROOT.ML
    44.5      ID:         $Id$
    44.6 -    Author:     Olaf Mueller
    44.7 -    Copyright   1998  TU Muenchen
    44.8 +    Author:     Olaf Müller
    44.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   44.10  
   44.11  Memory storage case study.
   44.12  *)
    45.1 --- a/src/HOLCF/IOA/Storage/Spec.thy	Thu Nov 15 23:25:01 2001 +0100
    45.2 +++ b/src/HOLCF/IOA/Storage/Spec.thy	Thu Nov 15 23:25:46 2001 +0100
    45.3 @@ -1,9 +1,9 @@
    45.4  (*  Title:      HOL/IOA/example/Spec.thy
    45.5      ID:         $Id$
    45.6 -    Author:     Olaf Mueller
    45.7 -    Copyright   1997  TU Muenchen
    45.8 +    Author:     Olaf Müller
    45.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   45.10  
   45.11 -The specification of a memory
   45.12 +The specification of a memory.
   45.13  *)
   45.14  
   45.15  Spec = IOA + Action +
    46.1 --- a/src/HOLCF/IOA/ex/ROOT.ML	Thu Nov 15 23:25:01 2001 +0100
    46.2 +++ b/src/HOLCF/IOA/ex/ROOT.ML	Thu Nov 15 23:25:46 2001 +0100
    46.3 @@ -1,7 +1,7 @@
    46.4  (*  Title:      HOL/IOA/ex/ROOT.ML
    46.5      ID:         $Id$
    46.6 -    Author:     Olaf Mueller
    46.7 -    Copyright   1997  TU Muenchen
    46.8 +    Author:     Olaf Müller
    46.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   46.10  
   46.11  This is the ROOT file for the formalization of a semantic model of
   46.12  I/O-Automata.  See the README.html file for details.
    47.1 --- a/src/HOLCF/IOA/ex/TrivEx.ML	Thu Nov 15 23:25:01 2001 +0100
    47.2 +++ b/src/HOLCF/IOA/ex/TrivEx.ML	Thu Nov 15 23:25:46 2001 +0100
    47.3 @@ -1,9 +1,9 @@
    47.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    47.5      ID:         $Id$
    47.6 -    Author:     Olaf Mueller
    47.7 -    Copyright   1995  TU Muenchen
    47.8 +    Author:     Olaf Müller
    47.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   47.10  
   47.11 -Trivial Abstraction Example
   47.12 +Trivial Abstraction Example.
   47.13  *)
   47.14  
   47.15  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    48.1 --- a/src/HOLCF/IOA/ex/TrivEx.thy	Thu Nov 15 23:25:01 2001 +0100
    48.2 +++ b/src/HOLCF/IOA/ex/TrivEx.thy	Thu Nov 15 23:25:46 2001 +0100
    48.3 @@ -1,9 +1,9 @@
    48.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    48.5      ID:         $Id$
    48.6 -    Author:     Olaf Mueller
    48.7 -    Copyright   1995  TU Muenchen
    48.8 +    Author:     Olaf Müller
    48.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   48.10  
   48.11 -Trivial Abstraction Example
   48.12 +Trivial Abstraction Example.
   48.13  *)
   48.14  
   48.15  TrivEx = Abstraction + 
    49.1 --- a/src/HOLCF/IOA/ex/TrivEx2.ML	Thu Nov 15 23:25:01 2001 +0100
    49.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Thu Nov 15 23:25:46 2001 +0100
    49.3 @@ -1,9 +1,9 @@
    49.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    49.5      ID:         $Id$
    49.6 -    Author:     Olaf Mueller
    49.7 -    Copyright   1995  TU Muenchen
    49.8 +    Author:     Olaf Müller
    49.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   49.10  
   49.11 -Trivial Abstraction Example
   49.12 +Trivial Abstraction Example.
   49.13  *)
   49.14  
   49.15  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    50.1 --- a/src/HOLCF/IOA/ex/TrivEx2.thy	Thu Nov 15 23:25:01 2001 +0100
    50.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy	Thu Nov 15 23:25:46 2001 +0100
    50.3 @@ -1,9 +1,9 @@
    50.4  (*  Title:      HOLCF/IOA/TrivEx.thy
    50.5      ID:         $Id$
    50.6 -    Author:     Olaf Mueller
    50.7 -    Copyright   1995  TU Muenchen
    50.8 +    Author:     Olaf Müller
    50.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   50.10  
   50.11 -Trivial Abstraction Example with fairness
   50.12 +Trivial Abstraction Example with fairness.
   50.13  *)
   50.14  
   50.15  TrivEx2 = Abstraction + IOA +
    51.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Nov 15 23:25:01 2001 +0100
    51.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Nov 15 23:25:46 2001 +0100
    51.3 @@ -1,13 +1,11 @@
    51.4  (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
    51.5      ID:         $Id$
    51.6 -    Author:     Olaf M"uller
    51.7 -    Copyright   1997  TU Muenchen
    51.8 +    Author:     Olaf Müller
    51.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   51.10  
   51.11 -Abstraction Theory -- tailored for I/O automata
   51.12 +Abstraction Theory -- tailored for I/O automata.
   51.13  *)   
   51.14  
   51.15 -
   51.16 -
   51.17  section "cex_abs";
   51.18  	
   51.19  
    52.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Nov 15 23:25:01 2001 +0100
    52.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Nov 15 23:25:46 2001 +0100
    52.3 @@ -1,9 +1,9 @@
    52.4  (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
    52.5      ID:         $Id$
    52.6 -    Author:     Olaf M"uller
    52.7 -    Copyright   1997  TU Muenchen
    52.8 +    Author:     Olaf Müller
    52.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   52.10  
   52.11 -Abstraction Theory -- tailored for I/O automata
   52.12 +Abstraction Theory -- tailored for I/O automata.
   52.13  *)   
   52.14  
   52.15  		       
    53.1 --- a/src/HOLCF/IOA/meta_theory/Asig.ML	Thu Nov 15 23:25:01 2001 +0100
    53.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Thu Nov 15 23:25:46 2001 +0100
    53.3 @@ -1,9 +1,9 @@
    53.4  (*  Title:      HOL/IOA/meta_theory/Asig.ML
    53.5      ID:         $Id$
    53.6 -    Author:     Olaf Mueller, Tobias Nipkow & Konrad Slind
    53.7 -    Copyright   1994,1996  TU Muenchen
    53.8 +    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    53.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   53.10  
   53.11 -Action signatures
   53.12 +Action signatures.
   53.13  *)
   53.14  
   53.15  val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
    54.1 --- a/src/HOLCF/IOA/meta_theory/Asig.thy	Thu Nov 15 23:25:01 2001 +0100
    54.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy	Thu Nov 15 23:25:46 2001 +0100
    54.3 @@ -1,9 +1,9 @@
    54.4  (*  Title:      HOL/IOA/meta_theory/Asig.thy
    54.5      ID:         $Id$
    54.6 -    Author:     Olaf Mueller, Tobias Nipkow & Konrad Slind
    54.7 -    Copyright   1994, 1996 TU Muenchen
    54.8 +    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    54.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   54.10  
   54.11 -Action signatures
   54.12 +Action signatures.
   54.13  *)
   54.14  
   54.15  Asig = Main +
    55.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Nov 15 23:25:01 2001 +0100
    55.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Nov 15 23:25:46 2001 +0100
    55.3 @@ -1,7 +1,7 @@
    55.4  (*  Title:      HOLCF/IOA/meta_theory/Automata.ML
    55.5      ID:         $Id$
    55.6      Author:     Olaf Mueller, Tobias Nipkow, Konrad Slind
    55.7 -    Copyright   1994, 1996  TU Muenchen
    55.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    55.9  
   55.10  The I/O automata of Lynch and Tuttle.
   55.11  *)
    56.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Nov 15 23:25:01 2001 +0100
    56.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Nov 15 23:25:46 2001 +0100
    56.3 @@ -1,7 +1,7 @@
    56.4  (*  Title:      HOLCF/IOA/meta_theory/Automata.thy
    56.5      ID:         $Id$
    56.6 -    Author:     Olaf M"uller, Konrad Slind, Tobias Nipkow
    56.7 -    Copyright   1995, 1996  TU Muenchen
    56.8 +    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
    56.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   56.10  
   56.11  The I/O automata of Lynch and Tuttle in HOLCF.
   56.12  *)   
    57.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Thu Nov 15 23:25:01 2001 +0100
    57.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Thu Nov 15 23:25:46 2001 +0100
    57.3 @@ -1,7 +1,7 @@
    57.4  (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
    57.5      ID:         $Id$
    57.6 -    Author:     Olaf M"uller
    57.7 -    Copyright   1996  TU Muenchen
    57.8 +    Author:     Olaf Müller
    57.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   57.10  
   57.11  Compositionality on Execution level.
   57.12  *)  
    58.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Nov 15 23:25:01 2001 +0100
    58.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Nov 15 23:25:46 2001 +0100
    58.3 @@ -1,7 +1,7 @@
    58.4  (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
    58.5      ID:         $Id$
    58.6 -    Author:     Olaf M"uller
    58.7 -    Copyright   1996  TU Muenchen
    58.8 +    Author:     Olaf Müller
    58.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   58.10  
   58.11  Compositionality on Execution level.
   58.12  *)  
    59.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Nov 15 23:25:01 2001 +0100
    59.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Nov 15 23:25:46 2001 +0100
    59.3 @@ -1,7 +1,7 @@
    59.4  (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.ML
    59.5      ID:         $Id$
    59.6 -    Author:     Olaf M"uller
    59.7 -    Copyright   1996  TU Muenchen
    59.8 +    Author:     Olaf Müller
    59.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   59.10  
   59.11  Compositionality on Schedule level.
   59.12  *) 
    60.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Nov 15 23:25:01 2001 +0100
    60.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Nov 15 23:25:46 2001 +0100
    60.3 @@ -1,7 +1,7 @@
    60.4  (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    60.5      ID:         $Id$
    60.6 -    Author:     Olaf M"uller
    60.7 -    Copyright   1996  TU Muenchen
    60.8 +    Author:     Olaf Müller
    60.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   60.10  
   60.11  Compositionality on Schedule level.
   60.12  *) 
    61.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Thu Nov 15 23:25:01 2001 +0100
    61.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Thu Nov 15 23:25:46 2001 +0100
    61.3 @@ -1,7 +1,7 @@
    61.4  (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.ML
    61.5      ID:		$Id$
    61.6 -    Author:     Olaf M"uller
    61.7 -    Copyright   1996  TU Muenchen
    61.8 +    Author:     Olaf Müller
    61.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   61.10   
   61.11  Compositionality on Trace level.
   61.12  *) 
    62.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Nov 15 23:25:01 2001 +0100
    62.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Nov 15 23:25:46 2001 +0100
    62.3 @@ -1,7 +1,7 @@
    62.4  (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
    62.5      ID:         $Id$
    62.6 -    Author:     Olaf M"uller
    62.7 -    Copyright   1996  TU Muenchen
    62.8 +    Author:     Olaf Müller
    62.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   62.10  
   62.11  Compositionality on Trace level.
   62.12  *) 
    63.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Nov 15 23:25:01 2001 +0100
    63.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Nov 15 23:25:46 2001 +0100
    63.3 @@ -1,7 +1,7 @@
    63.4  (*  Title:      HOLCF/IOA/meta_theory/Compositionality.ML
    63.5      ID:         $Id$
    63.6 -    Author:     Olaf M"uller
    63.7 -    Copyright   1997  TU Muenchen
    63.8 +    Author:     Olaf Müller
    63.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   63.10  
   63.11  Compositionality of I/O automata
   63.12  *) 
    64.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.thy	Thu Nov 15 23:25:01 2001 +0100
    64.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Thu Nov 15 23:25:46 2001 +0100
    64.3 @@ -1,9 +1,9 @@
    64.4  (*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
    64.5      ID:         $Id$
    64.6 -    Author:     Olaf M"uller
    64.7 -    Copyright   1997  TU Muenchen
    64.8 +    Author:     Olaf Müller
    64.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   64.10  
   64.11 -Compositionality of I/O automata
   64.12 +Compositionality of I/O automata.
   64.13  *) 
   64.14  
   64.15  Compositionality = CompoTraces
    65.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Thu Nov 15 23:25:01 2001 +0100
    65.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Thu Nov 15 23:25:46 2001 +0100
    65.3 @@ -1,9 +1,9 @@
    65.4  (*  Title:      HOLCF/IOA/meta_theory/Deadlock.ML
    65.5      ID:         $Id$
    65.6 -    Author:     Olaf Mueller
    65.7 -    Copyright   1997 TU Muenchen
    65.8 +    Author:     Olaf Müller
    65.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   65.10  
   65.11 -Deadlock freedom of I/O Automata
   65.12 +Deadlock freedom of I/O Automata.
   65.13  *)   
   65.14  
   65.15  (********************************************************************************
    66.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Nov 15 23:25:01 2001 +0100
    66.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Nov 15 23:25:46 2001 +0100
    66.3 @@ -1,9 +1,9 @@
    66.4  (*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
    66.5      ID:         $Id$
    66.6 -    Author:     Olaf Mueller
    66.7 -    Copyright   1997 TU Muenchen
    66.8 +    Author:     Olaf Müller
    66.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   66.10  
   66.11 -Deadlock freedom of I/O Automata
   66.12 +Deadlock freedom of I/O Automata.
   66.13  *)   
   66.14  
   66.15  Deadlock = RefCorrectness + CompoScheds
    67.1 --- a/src/HOLCF/IOA/meta_theory/IOA.ML	Thu Nov 15 23:25:01 2001 +0100
    67.2 +++ b/src/HOLCF/IOA/meta_theory/IOA.ML	Thu Nov 15 23:25:46 2001 +0100
    67.3 @@ -1,7 +1,7 @@
    67.4  (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    67.5      ID:         $Id$
    67.6 -    Author:     Olaf Mueller
    67.7 -    Copyright   1996,1997  TU Muenchen
    67.8 +    Author:     Olaf Müller
    67.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   67.10  
   67.11  The theory of I/O automata in HOLCF.
   67.12  *)  
    68.1 --- a/src/HOLCF/IOA/meta_theory/IOA.thy	Thu Nov 15 23:25:01 2001 +0100
    68.2 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy	Thu Nov 15 23:25:46 2001 +0100
    68.3 @@ -1,13 +1,9 @@
    68.4  (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    68.5      ID:         $Id$
    68.6 -    Author:     Olaf Mueller
    68.7 -    Copyright   1996,1997  TU Muenchen
    68.8 +    Author:     Olaf Müller
    68.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   68.10  
   68.11  The theory of I/O automata in HOLCF.
   68.12  *)   
   68.13 -
   68.14 - 
   68.15  	       
   68.16  IOA = SimCorrectness + Compositionality + Deadlock
   68.17 -
   68.18 -
    69.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Nov 15 23:25:01 2001 +0100
    69.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Nov 15 23:25:46 2001 +0100
    69.3 @@ -1,10 +1,9 @@
    69.4  (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.ML
    69.5      ID:         $Id$
    69.6 -    Author:     Olaf M"uller
    69.7 -    Copyright   1997  TU Muenchen
    69.8 +    Author:     Olaf Müller
    69.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   69.10  
   69.11 -Live I/O Automata
   69.12 -
   69.13 +Live I/O Automata.
   69.14  *)   
   69.15  
   69.16  Delsimps [split_paired_Ex];
    70.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Nov 15 23:25:01 2001 +0100
    70.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Nov 15 23:25:46 2001 +0100
    70.3 @@ -1,10 +1,9 @@
    70.4  (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
    70.5      ID:         $Id$
    70.6 -    Author:     Olaf M"uller
    70.7 -    Copyright   1997  TU Muenchen
    70.8 +    Author:     Olaf Müller
    70.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   70.10  
   70.11 -Live I/O automata -- specified by temproal formulas
   70.12 -
   70.13 +Live I/O automata -- specified by temproal formulas.
   70.14  *) 
   70.15    
   70.16  LiveIOA = TLS + 
    71.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Nov 15 23:25:01 2001 +0100
    71.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Thu Nov 15 23:25:46 2001 +0100
    71.3 @@ -1,10 +1,9 @@
    71.4  (*  Title:      HOLCF/IOA/meta_theory/Pred.thy
    71.5      ID:         $Id$
    71.6 -    Author:     Olaf M"uller
    71.7 -    Copyright   1997  TU Muenchen
    71.8 +    Author:     Olaf Müller
    71.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   71.10  
   71.11  Logical Connectives lifted to predicates.
   71.12 -
   71.13  *)   
   71.14  	       
   71.15  Pred = Main +
    72.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Nov 15 23:25:01 2001 +0100
    72.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Nov 15 23:25:46 2001 +0100
    72.3 @@ -1,9 +1,9 @@
    72.4  (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.ML
    72.5      ID:         $Id$
    72.6 -    Author:     Olaf Mueller
    72.7 -    Copyright   1996  TU Muenchen
    72.8 +    Author:     Olaf Müller
    72.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   72.10  
   72.11 -Correctness of Refinement Mappings in HOLCF/IOA
   72.12 +Correctness of Refinement Mappings in HOLCF/IOA.
   72.13  *)
   72.14  
   72.15  
    73.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Nov 15 23:25:01 2001 +0100
    73.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Nov 15 23:25:46 2001 +0100
    73.3 @@ -1,9 +1,9 @@
    73.4  (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
    73.5      ID:         $Id$
    73.6 -    Author:     Olaf Mueller
    73.7 -    Copyright   1996  TU Muenchen
    73.8 +    Author:     Olaf Müller
    73.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   73.10  
   73.11 -Correctness of Refinement Mappings in HOLCF/IOA
   73.12 +Correctness of Refinement Mappings in HOLCF/IOA.
   73.13  *)
   73.14  
   73.15  
    74.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Nov 15 23:25:01 2001 +0100
    74.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Nov 15 23:25:46 2001 +0100
    74.3 @@ -1,15 +1,12 @@
    74.4  (*  Title:      HOLCF/IOA/meta_theory/RefMappings.ML
    74.5      ID:         $Id$
    74.6 -    Author:     Olaf Mueller
    74.7 -    Copyright   1996  TU Muenchen
    74.8 +    Author:     Olaf Müller
    74.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   74.10  
   74.11 -Refinement Mappings in HOLCF/IOA
   74.12 +Refinement Mappings in HOLCF/IOA.
   74.13  *)
   74.14  
   74.15  
   74.16 -
   74.17 -
   74.18 -
   74.19  (* ---------------------------------------------------------------------------- *)
   74.20  
   74.21  section "transitions and moves";
    75.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Thu Nov 15 23:25:01 2001 +0100
    75.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Thu Nov 15 23:25:46 2001 +0100
    75.3 @@ -1,9 +1,9 @@
    75.4  (*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
    75.5      ID:         $Id$
    75.6 -    Author:     Olaf Mueller
    75.7 -    Copyright   1996  TU Muenchen
    75.8 +    Author:     Olaf Müller
    75.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   75.10  
   75.11 -Refinement Mappings in HOLCF/IOA
   75.12 +Refinement Mappings in HOLCF/IOA.
   75.13  *)
   75.14  
   75.15  RefMappings = Traces  +
    76.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Nov 15 23:25:01 2001 +0100
    76.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Nov 15 23:25:46 2001 +0100
    76.3 @@ -1,8 +1,7 @@
    76.4  (*  Title:      HOLCF/IOA/meta_theory/Seq.ML
    76.5      ID:         $Id$
    76.6 -    Author:     Olaf M"uller
    76.7 -    Copyright   1996  TU Muenchen
    76.8 -
    76.9 +    Author:     Olaf Müller
   76.10 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   76.11  *)  
   76.12  
   76.13  Addsimps (sfinite.intrs @ seq.rews);
    77.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Nov 15 23:25:01 2001 +0100
    77.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Nov 15 23:25:46 2001 +0100
    77.3 @@ -1,7 +1,7 @@
    77.4  (*  Title:      HOLCF/IOA/meta_theory/Seq.thy
    77.5      ID:         $Id$
    77.6 -    Author:     Olaf M"uller
    77.7 -    Copyright   1996  TU Muenchen
    77.8 +    Author:     Olaf Müller
    77.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   77.10  
   77.11  Partial, Finite and Infinite Sequences (lazy lists), modeled as domain.
   77.12  *)  
    78.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Nov 15 23:25:01 2001 +0100
    78.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Nov 15 23:25:46 2001 +0100
    78.3 @@ -1,10 +1,9 @@
    78.4  (*  Title:      HOLCF/IOA/meta_theory/Sequence.ML
    78.5      ID:         $Id$
    78.6 -    Author:     Olaf M"uller
    78.7 -    Copyright   1996  TU Muenchen
    78.8 +    Author:     Olaf Müller
    78.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   78.10  
   78.11 -Theorems about Sequences over flat domains with lifted elements
   78.12 -
   78.13 +Theorems about Sequences over flat domains with lifted elements.
   78.14  *)
   78.15  
   78.16  
    79.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Nov 15 23:25:01 2001 +0100
    79.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Nov 15 23:25:46 2001 +0100
    79.3 @@ -1,10 +1,9 @@
    79.4  (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    79.5      ID:         $Id$
    79.6 -    Author:     Olaf M"uller
    79.7 -    Copyright   1996  TU Muenchen
    79.8 +    Author:     Olaf Müller
    79.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   79.10  
   79.11 -Sequences over flat domains with lifted elements
   79.12 -
   79.13 +Sequences over flat domains with lifted elements.
   79.14  *)  
   79.15  
   79.16  Sequence = Seq + 
    80.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Nov 15 23:25:01 2001 +0100
    80.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Thu Nov 15 23:25:46 2001 +0100
    80.3 @@ -1,13 +1,12 @@
    80.4  (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    80.5      ID:         $Id$
    80.6 -    Author:     Olaf M"uller
    80.7 -    Copyright   1997  TU Muenchen
    80.8 +    Author:     Olaf Müller
    80.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   80.10  
   80.11  Some properties about (Cut ex), defined as follows:
   80.12  
   80.13  For every execution ex there is another shorter execution (Cut ex) 
   80.14  that has the same trace as ex, but its schedule ends with an external action.
   80.15 -
   80.16  *) 
   80.17  
   80.18  
    81.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Nov 15 23:25:01 2001 +0100
    81.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Nov 15 23:25:46 2001 +0100
    81.3 @@ -1,13 +1,12 @@
    81.4  (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    81.5      ID:         $Id$
    81.6 -    Author:     Olaf M"uller
    81.7 -    Copyright   1997  TU Muenchen
    81.8 +    Author:     Olaf Müller
    81.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   81.10  
   81.11  Some properties about (Cut ex), defined as follows:
   81.12  
   81.13  For every execution ex there is another shorter execution (Cut ex) 
   81.14  that has the same trace as ex, but its schedule ends with an external action.
   81.15 -
   81.16  *) 
   81.17  
   81.18  
    82.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Thu Nov 15 23:25:01 2001 +0100
    82.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Thu Nov 15 23:25:46 2001 +0100
    82.3 @@ -1,9 +1,9 @@
    82.4  (*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.ML
    82.5      ID:         $Id$
    82.6 -    Author:     Olaf Mueller
    82.7 -    Copyright   1996  TU Muenchen
    82.8 +    Author:     Olaf Müller
    82.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   82.10  
   82.11 -Correctness of Simulations in HOLCF/IOA
   82.12 +Correctness of Simulations in HOLCF/IOA.
   82.13  *)
   82.14  
   82.15  
    83.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Nov 15 23:25:01 2001 +0100
    83.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Nov 15 23:25:46 2001 +0100
    83.3 @@ -1,9 +1,9 @@
    83.4  (*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
    83.5      ID:         $Id$
    83.6 -    Author:     Olaf Mueller
    83.7 -    Copyright   1997  TU Muenchen
    83.8 +    Author:     Olaf Müller
    83.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   83.10  
   83.11 -Correctness of Simulations in HOLCF/IOA
   83.12 +Correctness of Simulations in HOLCF/IOA.
   83.13  *)
   83.14  
   83.15  
    84.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Thu Nov 15 23:25:01 2001 +0100
    84.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Thu Nov 15 23:25:46 2001 +0100
    84.3 @@ -1,9 +1,9 @@
    84.4  (*  Title:      HOLCF/IOA/meta_theory/Simulations.ML
    84.5      ID:         $Id$
    84.6 -    Author:     Olaf Mueller
    84.7 -    Copyright   1997  TU Muenchen
    84.8 +    Author:     Olaf Müller
    84.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   84.10  
   84.11 -Simulations in HOLCF/IOA
   84.12 +Simulations in HOLCF/IOA.
   84.13  *)
   84.14  
   84.15  
    85.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Thu Nov 15 23:25:01 2001 +0100
    85.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Thu Nov 15 23:25:46 2001 +0100
    85.3 @@ -1,9 +1,9 @@
    85.4  (*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
    85.5      ID:         $Id$
    85.6 -    Author:     Olaf Mueller
    85.7 -    Copyright   1997  TU Muenchen
    85.8 +    Author:     Olaf Müller
    85.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   85.10  
   85.11 -Simulations in HOLCF/IOA
   85.12 +Simulations in HOLCF/IOA.
   85.13  *)
   85.14  
   85.15  Simulations = RefCorrectness  +
    86.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Thu Nov 15 23:25:01 2001 +0100
    86.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Thu Nov 15 23:25:46 2001 +0100
    86.3 @@ -1,9 +1,9 @@
    86.4  (*  Title:      HOLCF/IOA/meta_theory/TL.ML
    86.5      ID:         $Id$
    86.6 -    Author:     Olaf M"uller
    86.7 -    Copyright   1997  TU Muenchen
    86.8 +    Author:     Olaf Müller
    86.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   86.10  
   86.11 -Temporal Logic 
   86.12 +Temporal Logic.
   86.13  *)   
   86.14  
   86.15  
    87.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Thu Nov 15 23:25:01 2001 +0100
    87.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Thu Nov 15 23:25:46 2001 +0100
    87.3 @@ -1,14 +1,11 @@
    87.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    87.5      ID:         $Id$
    87.6 -    Author:     Olaf M"uller
    87.7 -    Copyright   1997  TU Muenchen
    87.8 -
    87.9 -A General Temporal Logic
   87.10 +    Author:     Olaf Müller
   87.11 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   87.12  
   87.13 +A General Temporal Logic.
   87.14  *)   
   87.15 -
   87.16 -
   87.17 -		       
   87.18 +	       
   87.19  TL = Pred + Sequence +  
   87.20  
   87.21  default term
    88.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Thu Nov 15 23:25:01 2001 +0100
    88.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Thu Nov 15 23:25:46 2001 +0100
    88.3 @@ -1,9 +1,9 @@
    88.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.ML
    88.5      ID:         $Id$
    88.6 -    Author:     Olaf M"uller
    88.7 -    Copyright   1997  TU Muenchen
    88.8 +    Author:     Olaf Müller
    88.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   88.10  
   88.11 -Temporal Logic of Steps -- tailored for I/O automata
   88.12 +Temporal Logic of Steps -- tailored for I/O automata.
   88.13  *)    
   88.14  
   88.15  (* global changes to simpset() and claset(), repeated from Traces.ML *)
    89.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Nov 15 23:25:01 2001 +0100
    89.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Nov 15 23:25:46 2001 +0100
    89.3 @@ -1,9 +1,9 @@
    89.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    89.5      ID:         $Id$
    89.6 -    Author:     Olaf M"uller
    89.7 -    Copyright   1997  TU Muenchen
    89.8 +    Author:     Olaf Müller
    89.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   89.10  
   89.11 -Temporal Logic of Steps -- tailored for I/O automata
   89.12 +Temporal Logic of Steps -- tailored for I/O automata.
   89.13  *)   
   89.14  
   89.15  		       
    90.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Thu Nov 15 23:25:01 2001 +0100
    90.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Thu Nov 15 23:25:46 2001 +0100
    90.3 @@ -1,7 +1,7 @@
    90.4  (*  Title:      HOLCF/IOA/meta_theory/Traces.ML
    90.5      ID:         $Id$
    90.6 -    Author:     Olaf M"uller
    90.7 -    Copyright   1996  TU Muenchen
    90.8 +    Author:     Olaf Müller
    90.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   90.10  
   90.11  Theorems about Executions and Traces of I/O automata in HOLCF.
   90.12  *)   
    91.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Nov 15 23:25:01 2001 +0100
    91.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Nov 15 23:25:46 2001 +0100
    91.3 @@ -1,7 +1,7 @@
    91.4  (*  Title:      HOLCF/IOA/meta_theory/Traces.thy
    91.5      ID:         $Id$
    91.6 -    Author:     Olaf M"uller
    91.7 -    Copyright   1996  TU Muenchen
    91.8 +    Author:     Olaf Müller
    91.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   91.10  
   91.11  Executions and Traces of I/O automata in HOLCF.
   91.12  *)