remove $ from all HOLCF files
authorhuffman
Wed Feb 17 10:00:22 2010 -0800 (2010-02-17 ago)
changeset 35174e15040ae75d7
parent 35170 bb1d1c6a10bb
child 35175 61255c81da01
remove $ from all HOLCF files
src/HOLCF/FOCUS/Buffer_adm.thy
src/HOLCF/FOCUS/FOCUS.thy
src/HOLCF/FOCUS/Stream_adm.thy
src/HOLCF/IMP/Denotational.thy
src/HOLCF/IMP/HoareEx.thy
src/HOLCF/IMP/README.html
src/HOLCF/IMP/ROOT.ML
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.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.thy
src/HOLCF/IOA/ABP/Packet.thy
src/HOLCF/IOA/ABP/Receiver.thy
src/HOLCF/IOA/ABP/Sender.thy
src/HOLCF/IOA/ABP/Spec.thy
src/HOLCF/IOA/Modelcheck/Cockpit.thy
src/HOLCF/IOA/Modelcheck/ROOT.ML
src/HOLCF/IOA/NTP/Abschannel.thy
src/HOLCF/IOA/NTP/Action.thy
src/HOLCF/IOA/NTP/Correctness.thy
src/HOLCF/IOA/NTP/Impl.thy
src/HOLCF/IOA/NTP/Lemmas.thy
src/HOLCF/IOA/NTP/Multiset.thy
src/HOLCF/IOA/NTP/Packet.thy
src/HOLCF/IOA/NTP/Receiver.thy
src/HOLCF/IOA/NTP/Sender.thy
src/HOLCF/IOA/NTP/Spec.thy
src/HOLCF/IOA/README.html
src/HOLCF/IOA/Storage/Action.thy
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/Storage/Impl.thy
src/HOLCF/IOA/Storage/Spec.thy
src/HOLCF/IOA/meta_theory/Asig.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOLCF/IOA/meta_theory/IOA.thy
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOLCF/IOA/meta_theory/Simulations.thy
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/README.html
src/HOLCF/ex/Dagstuhl.thy
src/HOLCF/ex/Fix2.thy
src/HOLCF/ex/Focus_ex.thy
src/HOLCF/ex/Hoare.thy
src/HOLCF/ex/Loop.thy
src/HOLCF/ex/Stream.thy
src/HOLCF/ex/hoare.txt
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.thy	Wed Feb 17 09:22:40 2010 -0800
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Wed Feb 17 10:00:22 2010 -0800
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOLCF/FOCUS/Buffer_adm.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb, TU Muenchen
     1.7  *)
     1.8  
     2.1 --- a/src/HOLCF/FOCUS/FOCUS.thy	Wed Feb 17 09:22:40 2010 -0800
     2.2 +++ b/src/HOLCF/FOCUS/FOCUS.thy	Wed Feb 17 10:00:22 2010 -0800
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOLCF/FOCUS/FOCUS.thy
     2.5 -    ID:         $Id$
     2.6      Author:     David von Oheimb, TU Muenchen
     2.7  *)
     2.8  
     3.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Wed Feb 17 09:22:40 2010 -0800
     3.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Wed Feb 17 10:00:22 2010 -0800
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOLCF/ex/Stream_adm.thy
     3.5 -    ID:         $Id$
     3.6      Author:     David von Oheimb, TU Muenchen
     3.7  *)
     3.8  
     4.1 --- a/src/HOLCF/IMP/Denotational.thy	Wed Feb 17 09:22:40 2010 -0800
     4.2 +++ b/src/HOLCF/IMP/Denotational.thy	Wed Feb 17 10:00:22 2010 -0800
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOLCF/IMP/Denotational.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Tobias Nipkow and Robert Sandner, TUM
     4.7      Copyright   1996 TUM
     4.8  *)
     5.1 --- a/src/HOLCF/IMP/HoareEx.thy	Wed Feb 17 09:22:40 2010 -0800
     5.2 +++ b/src/HOLCF/IMP/HoareEx.thy	Wed Feb 17 10:00:22 2010 -0800
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOLCF/IMP/HoareEx.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow, TUM
     5.7      Copyright   1997 TUM
     5.8  *)
     6.1 --- a/src/HOLCF/IMP/README.html	Wed Feb 17 09:22:40 2010 -0800
     6.2 +++ b/src/HOLCF/IMP/README.html	Wed Feb 17 10:00:22 2010 -0800
     6.3 @@ -1,7 +1,5 @@
     6.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     6.5  
     6.6 -<!-- $Id$ -->
     6.7 -
     6.8  <HTML>
     6.9  
    6.10  <HEAD>
     7.1 --- a/src/HOLCF/IMP/ROOT.ML	Wed Feb 17 09:22:40 2010 -0800
     7.2 +++ b/src/HOLCF/IMP/ROOT.ML	Wed Feb 17 10:00:22 2010 -0800
     7.3 @@ -1,3 +1,1 @@
     7.4 -(* $Id$ *)
     7.5 -
     7.6  use_thys ["HoareEx"];
     8.1 --- a/src/HOLCF/IOA/ABP/Abschannel.thy	Wed Feb 17 09:22:40 2010 -0800
     8.2 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy	Wed Feb 17 10:00:22 2010 -0800
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOLCF/IOA/ABP/Abschannel.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Olaf Müller
     8.7  *)
     8.8  
     9.1 --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Wed Feb 17 09:22:40 2010 -0800
     9.2 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Wed Feb 17 10:00:22 2010 -0800
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOLCF/IOA/ABP/Abschannels.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Olaf Müller
     9.7  *)
     9.8  
    10.1 --- a/src/HOLCF/IOA/ABP/Action.thy	Wed Feb 17 09:22:40 2010 -0800
    10.2 +++ b/src/HOLCF/IOA/ABP/Action.thy	Wed Feb 17 10:00:22 2010 -0800
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOLCF/IOA/ABP/Action.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Olaf Müller
    10.7  *)
    10.8  
    11.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Wed Feb 17 09:22:40 2010 -0800
    11.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Wed Feb 17 10:00:22 2010 -0800
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOLCF/IOA/ABP/Check.ML
    11.5 -    ID:         $Id$
    11.6      Author:     Olaf Mueller
    11.7  
    11.8  The Model Checker.
    12.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Wed Feb 17 09:22:40 2010 -0800
    12.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Wed Feb 17 10:00:22 2010 -0800
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      HOLCF/IOA/ABP/Correctness.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Olaf Müller
    12.7  *)
    12.8  
    13.1 --- a/src/HOLCF/IOA/ABP/Env.thy	Wed Feb 17 09:22:40 2010 -0800
    13.2 +++ b/src/HOLCF/IOA/ABP/Env.thy	Wed Feb 17 10:00:22 2010 -0800
    13.3 @@ -1,5 +1,4 @@
    13.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
    13.5 -    ID:         $Id$
    13.6      Author:     Olaf Müller
    13.7  *)
    13.8  
    14.1 --- a/src/HOLCF/IOA/ABP/Impl.thy	Wed Feb 17 09:22:40 2010 -0800
    14.2 +++ b/src/HOLCF/IOA/ABP/Impl.thy	Wed Feb 17 10:00:22 2010 -0800
    14.3 @@ -1,5 +1,4 @@
    14.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
    14.5 -    ID:         $Id$
    14.6      Author:     Olaf Müller
    14.7  *)
    14.8  
    15.1 --- a/src/HOLCF/IOA/ABP/Impl_finite.thy	Wed Feb 17 09:22:40 2010 -0800
    15.2 +++ b/src/HOLCF/IOA/ABP/Impl_finite.thy	Wed Feb 17 10:00:22 2010 -0800
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      HOLCF/IOA/ABP/Impl.thy
    15.5 -    ID:         $Id$
    15.6      Author:     Olaf Müller
    15.7  *)
    15.8  
    16.1 --- a/src/HOLCF/IOA/ABP/Lemmas.thy	Wed Feb 17 09:22:40 2010 -0800
    16.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Wed Feb 17 10:00:22 2010 -0800
    16.3 @@ -1,5 +1,4 @@
    16.4  (*  Title:      HOLCF/IOA/ABP/Lemmas.thy
    16.5 -    ID:         $Id$
    16.6      Author:     Olaf Müller
    16.7  *)
    16.8  
    17.1 --- a/src/HOLCF/IOA/ABP/Packet.thy	Wed Feb 17 09:22:40 2010 -0800
    17.2 +++ b/src/HOLCF/IOA/ABP/Packet.thy	Wed Feb 17 10:00:22 2010 -0800
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      HOLCF/IOA/ABP/Packet.thy
    17.5 -    ID:         $Id$
    17.6      Author:     Olaf Müller
    17.7  *)
    17.8  
    18.1 --- a/src/HOLCF/IOA/ABP/Receiver.thy	Wed Feb 17 09:22:40 2010 -0800
    18.2 +++ b/src/HOLCF/IOA/ABP/Receiver.thy	Wed Feb 17 10:00:22 2010 -0800
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      HOLCF/IOA/ABP/Receiver.thy
    18.5 -    ID:         $Id$
    18.6      Author:     Olaf Müller
    18.7  *)
    18.8  
    19.1 --- a/src/HOLCF/IOA/ABP/Sender.thy	Wed Feb 17 09:22:40 2010 -0800
    19.2 +++ b/src/HOLCF/IOA/ABP/Sender.thy	Wed Feb 17 10:00:22 2010 -0800
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      HOLCF/IOA/ABP/Sender.thy
    19.5 -    ID:         $Id$
    19.6      Author:     Olaf Müller
    19.7  *)
    19.8  
    20.1 --- a/src/HOLCF/IOA/ABP/Spec.thy	Wed Feb 17 09:22:40 2010 -0800
    20.2 +++ b/src/HOLCF/IOA/ABP/Spec.thy	Wed Feb 17 10:00:22 2010 -0800
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      HOLCF/IOA/ABP/Spec.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Olaf Müller
    20.7  *)
    20.8  
    21.1 --- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Wed Feb 17 09:22:40 2010 -0800
    21.2 +++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy	Wed Feb 17 10:00:22 2010 -0800
    21.3 @@ -1,6 +1,3 @@
    21.4 -
    21.5 -(* $Id$ *)
    21.6 -
    21.7  theory Cockpit
    21.8  imports MuIOAOracle
    21.9  begin
    22.1 --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Wed Feb 17 09:22:40 2010 -0800
    22.2 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Wed Feb 17 10:00:22 2010 -0800
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOLCF/IOA/Modelcheck/ROOT.ML
    22.5 -    ID:         $Id$
    22.6      Author:     Olaf Mueller and Tobias Hamberger, TU Muenchen
    22.7  
    22.8  Modelchecker setup for I/O automata.
    23.1 --- a/src/HOLCF/IOA/NTP/Abschannel.thy	Wed Feb 17 09:22:40 2010 -0800
    23.2 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy	Wed Feb 17 10:00:22 2010 -0800
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      HOL/IOA/NTP/Abschannel.thy
    23.5 -    ID:         $Id$
    23.6      Author:     Olaf Müller
    23.7  *)
    23.8  
    24.1 --- a/src/HOLCF/IOA/NTP/Action.thy	Wed Feb 17 09:22:40 2010 -0800
    24.2 +++ b/src/HOLCF/IOA/NTP/Action.thy	Wed Feb 17 10:00:22 2010 -0800
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      HOL/IOA/NTP/Action.thy
    24.5 -    ID:         $Id$
    24.6      Author:     Tobias Nipkow & Konrad Slind
    24.7  *)
    24.8  
    25.1 --- a/src/HOLCF/IOA/NTP/Correctness.thy	Wed Feb 17 09:22:40 2010 -0800
    25.2 +++ b/src/HOLCF/IOA/NTP/Correctness.thy	Wed Feb 17 10:00:22 2010 -0800
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      HOL/IOA/NTP/Correctness.thy
    25.5 -    ID:         $Id$
    25.6      Author:     Tobias Nipkow & Konrad Slind
    25.7  *)
    25.8  
    26.1 --- a/src/HOLCF/IOA/NTP/Impl.thy	Wed Feb 17 09:22:40 2010 -0800
    26.2 +++ b/src/HOLCF/IOA/NTP/Impl.thy	Wed Feb 17 10:00:22 2010 -0800
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:      HOL/IOA/NTP/Impl.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Tobias Nipkow & Konrad Slind
    26.7  *)
    26.8  
    27.1 --- a/src/HOLCF/IOA/NTP/Lemmas.thy	Wed Feb 17 09:22:40 2010 -0800
    27.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.thy	Wed Feb 17 10:00:22 2010 -0800
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      HOL/IOA/NTP/Lemmas.thy
    27.5 -    ID:         $Id$
    27.6      Author:     Tobias Nipkow & Konrad Slind
    27.7  *)
    27.8  
    28.1 --- a/src/HOLCF/IOA/NTP/Multiset.thy	Wed Feb 17 09:22:40 2010 -0800
    28.2 +++ b/src/HOLCF/IOA/NTP/Multiset.thy	Wed Feb 17 10:00:22 2010 -0800
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      HOL/IOA/NTP/Multiset.thy
    28.5 -    ID:         $Id$
    28.6      Author:     Tobias Nipkow & Konrad Slind
    28.7  *)
    28.8  
    29.1 --- a/src/HOLCF/IOA/NTP/Packet.thy	Wed Feb 17 09:22:40 2010 -0800
    29.2 +++ b/src/HOLCF/IOA/NTP/Packet.thy	Wed Feb 17 10:00:22 2010 -0800
    29.3 @@ -1,5 +1,4 @@
    29.4  (*  Title:      HOL/IOA/NTP/Packet.thy
    29.5 -    ID:         $Id$
    29.6      Author:     Tobias Nipkow & Konrad Slind
    29.7  *)
    29.8  
    30.1 --- a/src/HOLCF/IOA/NTP/Receiver.thy	Wed Feb 17 09:22:40 2010 -0800
    30.2 +++ b/src/HOLCF/IOA/NTP/Receiver.thy	Wed Feb 17 10:00:22 2010 -0800
    30.3 @@ -1,5 +1,4 @@
    30.4  (*  Title:      HOL/IOA/NTP/Receiver.thy
    30.5 -    ID:         $Id$
    30.6      Author:     Tobias Nipkow & Konrad Slind
    30.7  *)
    30.8  
    31.1 --- a/src/HOLCF/IOA/NTP/Sender.thy	Wed Feb 17 09:22:40 2010 -0800
    31.2 +++ b/src/HOLCF/IOA/NTP/Sender.thy	Wed Feb 17 10:00:22 2010 -0800
    31.3 @@ -1,5 +1,4 @@
    31.4  (*  Title:      HOL/IOA/NTP/Sender.thy
    31.5 -    ID:         $Id$
    31.6      Author:     Tobias Nipkow & Konrad Slind
    31.7  *)
    31.8  
    32.1 --- a/src/HOLCF/IOA/NTP/Spec.thy	Wed Feb 17 09:22:40 2010 -0800
    32.2 +++ b/src/HOLCF/IOA/NTP/Spec.thy	Wed Feb 17 10:00:22 2010 -0800
    32.3 @@ -1,5 +1,4 @@
    32.4  (*  Title:      HOL/IOA/NTP/Spec.thy
    32.5 -    ID:         $Id$
    32.6      Author:     Tobias Nipkow & Konrad Slind
    32.7  *)
    32.8  
    33.1 --- a/src/HOLCF/IOA/README.html	Wed Feb 17 09:22:40 2010 -0800
    33.2 +++ b/src/HOLCF/IOA/README.html	Wed Feb 17 10:00:22 2010 -0800
    33.3 @@ -1,7 +1,5 @@
    33.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    33.5  
    33.6 -<!-- $Id$ -->
    33.7 -
    33.8  <HTML>
    33.9  
   33.10  <HEAD>
    34.1 --- a/src/HOLCF/IOA/Storage/Action.thy	Wed Feb 17 09:22:40 2010 -0800
    34.2 +++ b/src/HOLCF/IOA/Storage/Action.thy	Wed Feb 17 10:00:22 2010 -0800
    34.3 @@ -1,5 +1,4 @@
    34.4  (*  Title:      HOLCF/IOA/ABP/Action.thy
    34.5 -    ID:         $Id$
    34.6      Author:     Olaf Müller
    34.7  *)
    34.8  
    35.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy	Wed Feb 17 09:22:40 2010 -0800
    35.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Wed Feb 17 10:00:22 2010 -0800
    35.3 @@ -1,5 +1,4 @@
    35.4  (*  Title:      HOL/IOA/example/Correctness.thy
    35.5 -    ID:         $Id$
    35.6      Author:     Olaf Müller
    35.7  *)
    35.8  
    36.1 --- a/src/HOLCF/IOA/Storage/Impl.thy	Wed Feb 17 09:22:40 2010 -0800
    36.2 +++ b/src/HOLCF/IOA/Storage/Impl.thy	Wed Feb 17 10:00:22 2010 -0800
    36.3 @@ -1,5 +1,4 @@
    36.4  (*  Title:      HOL/IOA/example/Spec.thy
    36.5 -    ID:         $Id$
    36.6      Author:     Olaf Müller
    36.7  *)
    36.8  
    37.1 --- a/src/HOLCF/IOA/Storage/Spec.thy	Wed Feb 17 09:22:40 2010 -0800
    37.2 +++ b/src/HOLCF/IOA/Storage/Spec.thy	Wed Feb 17 10:00:22 2010 -0800
    37.3 @@ -1,5 +1,4 @@
    37.4  (*  Title:      HOL/IOA/example/Spec.thy
    37.5 -    ID:         $Id$
    37.6      Author:     Olaf Müller
    37.7  *)
    37.8  
    38.1 --- a/src/HOLCF/IOA/meta_theory/Asig.thy	Wed Feb 17 09:22:40 2010 -0800
    38.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy	Wed Feb 17 10:00:22 2010 -0800
    38.3 @@ -1,5 +1,4 @@
    38.4  (*  Title:      HOL/IOA/meta_theory/Asig.thy
    38.5 -    ID:         $Id$
    38.6      Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    38.7  *)
    38.8  
    39.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Feb 17 09:22:40 2010 -0800
    39.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Feb 17 10:00:22 2010 -0800
    39.3 @@ -1,5 +1,4 @@
    39.4  (*  Title:      HOLCF/IOA/meta_theory/Automata.thy
    39.5 -    ID:         $Id$
    39.6      Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
    39.7  *)
    39.8  
    40.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Feb 17 09:22:40 2010 -0800
    40.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Feb 17 10:00:22 2010 -0800
    40.3 @@ -1,5 +1,4 @@
    40.4  (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
    40.5 -    ID:         $Id$
    40.6      Author:     Olaf Müller
    40.7  *)
    40.8  
    41.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Feb 17 09:22:40 2010 -0800
    41.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Feb 17 10:00:22 2010 -0800
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    41.5 -    ID:         $Id$
    41.6      Author:     Olaf Müller
    41.7  *)
    41.8  
    42.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Feb 17 09:22:40 2010 -0800
    42.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Feb 17 10:00:22 2010 -0800
    42.3 @@ -1,5 +1,4 @@
    42.4  (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
    42.5 -    ID:         $Id$
    42.6      Author:     Olaf Müller
    42.7  *) 
    42.8  
    43.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Feb 17 09:22:40 2010 -0800
    43.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Feb 17 10:00:22 2010 -0800
    43.3 @@ -1,5 +1,4 @@
    43.4  (*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
    43.5 -    ID:         $Id$
    43.6      Author:     Olaf Müller
    43.7  *)
    43.8  
    44.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Feb 17 09:22:40 2010 -0800
    44.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Feb 17 10:00:22 2010 -0800
    44.3 @@ -1,5 +1,4 @@
    44.4  (*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
    44.5 -    ID:         $Id$
    44.6      Author:     Olaf Müller
    44.7  *)
    44.8  
    45.1 --- a/src/HOLCF/IOA/meta_theory/IOA.thy	Wed Feb 17 09:22:40 2010 -0800
    45.2 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy	Wed Feb 17 10:00:22 2010 -0800
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    45.5 -    ID:         $Id$
    45.6      Author:     Olaf Müller
    45.7  *)
    45.8  
    46.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Feb 17 09:22:40 2010 -0800
    46.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Feb 17 10:00:22 2010 -0800
    46.3 @@ -1,5 +1,4 @@
    46.4  (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
    46.5 -    ID:         $Id$
    46.6      Author:     Olaf Müller
    46.7  *)
    46.8  
    47.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Feb 17 09:22:40 2010 -0800
    47.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Feb 17 10:00:22 2010 -0800
    47.3 @@ -1,5 +1,4 @@
    47.4  (*  Title:      HOLCF/IOA/meta_theory/Pred.thy
    47.5 -    ID:         $Id$
    47.6      Author:     Olaf Müller
    47.7  *)
    47.8  
    48.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed Feb 17 09:22:40 2010 -0800
    48.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed Feb 17 10:00:22 2010 -0800
    48.3 @@ -1,5 +1,4 @@
    48.4  (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
    48.5 -    ID:         $Id$
    48.6      Author:     Olaf Müller
    48.7  *)
    48.8  
    49.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Feb 17 09:22:40 2010 -0800
    49.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Feb 17 10:00:22 2010 -0800
    49.3 @@ -1,5 +1,4 @@
    49.4  (*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
    49.5 -    ID:         $Id$
    49.6      Author:     Olaf Müller
    49.7  *)
    49.8  
    50.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Feb 17 09:22:40 2010 -0800
    50.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Feb 17 10:00:22 2010 -0800
    50.3 @@ -1,5 +1,4 @@
    50.4  (*  Title:      HOLCF/IOA/meta_theory/Seq.thy
    50.5 -    ID:         $Id$
    50.6      Author:     Olaf Müller
    50.7  *)
    50.8  
    51.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Feb 17 09:22:40 2010 -0800
    51.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Feb 17 10:00:22 2010 -0800
    51.3 @@ -1,5 +1,4 @@
    51.4  (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    51.5 -    ID:         $Id$
    51.6      Author:     Olaf Müller
    51.7  *)
    51.8  
    52.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Feb 17 09:22:40 2010 -0800
    52.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Feb 17 10:00:22 2010 -0800
    52.3 @@ -1,5 +1,4 @@
    52.4  (*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
    52.5 -    ID:         $Id$
    52.6      Author:     Olaf Müller
    52.7  *)
    52.8  
    53.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Wed Feb 17 09:22:40 2010 -0800
    53.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Wed Feb 17 10:00:22 2010 -0800
    53.3 @@ -1,5 +1,4 @@
    53.4  (*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
    53.5 -    ID:         $Id$
    53.6      Author:     Olaf Müller
    53.7  *)
    53.8  
    54.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Wed Feb 17 09:22:40 2010 -0800
    54.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Wed Feb 17 10:00:22 2010 -0800
    54.3 @@ -1,5 +1,4 @@
    54.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    54.5 -    ID:         $Id$
    54.6      Author:     Olaf Müller
    54.7  *)
    54.8  
    55.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Feb 17 09:22:40 2010 -0800
    55.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Feb 17 10:00:22 2010 -0800
    55.3 @@ -1,5 +1,4 @@
    55.4  (*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    55.5 -    ID:         $Id$
    55.6      Author:     Olaf Müller
    55.7  *)
    55.8  
    56.1 --- a/src/HOLCF/README.html	Wed Feb 17 09:22:40 2010 -0800
    56.2 +++ b/src/HOLCF/README.html	Wed Feb 17 10:00:22 2010 -0800
    56.3 @@ -1,7 +1,5 @@
    56.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    56.5  
    56.6 -<!-- $Id$ -->
    56.7 -
    56.8  <html>
    56.9  
   56.10  <head>
    57.1 --- a/src/HOLCF/ex/Dagstuhl.thy	Wed Feb 17 09:22:40 2010 -0800
    57.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Wed Feb 17 10:00:22 2010 -0800
    57.3 @@ -1,5 +1,3 @@
    57.4 -(* $Id$ *)
    57.5 -
    57.6  theory Dagstuhl
    57.7  imports Stream
    57.8  begin
    58.1 --- a/src/HOLCF/ex/Fix2.thy	Wed Feb 17 09:22:40 2010 -0800
    58.2 +++ b/src/HOLCF/ex/Fix2.thy	Wed Feb 17 10:00:22 2010 -0800
    58.3 @@ -1,5 +1,4 @@
    58.4  (*  Title:      HOLCF/ex/Fix2.thy
    58.5 -    ID:         $Id$
    58.6      Author:     Franz Regensburger
    58.7  
    58.8  Show that fix is the unique least fixed-point operator.
    59.1 --- a/src/HOLCF/ex/Focus_ex.thy	Wed Feb 17 09:22:40 2010 -0800
    59.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Wed Feb 17 10:00:22 2010 -0800
    59.3 @@ -1,5 +1,3 @@
    59.4 -(* $Id$ *)
    59.5 -
    59.6  (* Specification of the following loop back device
    59.7  
    59.8  
    60.1 --- a/src/HOLCF/ex/Hoare.thy	Wed Feb 17 09:22:40 2010 -0800
    60.2 +++ b/src/HOLCF/ex/Hoare.thy	Wed Feb 17 10:00:22 2010 -0800
    60.3 @@ -1,5 +1,4 @@
    60.4  (*  Title:      HOLCF/ex/hoare.thy
    60.5 -    ID:         $Id$
    60.6      Author:     Franz Regensburger
    60.7  
    60.8  Theory for an example by C.A.R. Hoare
    61.1 --- a/src/HOLCF/ex/Loop.thy	Wed Feb 17 09:22:40 2010 -0800
    61.2 +++ b/src/HOLCF/ex/Loop.thy	Wed Feb 17 10:00:22 2010 -0800
    61.3 @@ -1,5 +1,4 @@
    61.4  (*  Title:      HOLCF/ex/Loop.thy
    61.5 -    ID:         $Id$
    61.6      Author:     Franz Regensburger
    61.7  *)
    61.8  
    62.1 --- a/src/HOLCF/ex/Stream.thy	Wed Feb 17 09:22:40 2010 -0800
    62.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Feb 17 10:00:22 2010 -0800
    62.3 @@ -1,5 +1,4 @@
    62.4  (*  Title:      HOLCF/ex/Stream.thy
    62.5 -    ID:         $Id$
    62.6      Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
    62.7  *)
    62.8  
    63.1 --- a/src/HOLCF/ex/hoare.txt	Wed Feb 17 09:22:40 2010 -0800
    63.2 +++ b/src/HOLCF/ex/hoare.txt	Wed Feb 17 10:00:22 2010 -0800
    63.3 @@ -1,5 +1,3 @@
    63.4 -(* $Id$ *)
    63.5 -
    63.6  Proves about loops and tail-recursive functions
    63.7  ===============================================
    63.8