tuned headers;
authorwenzelm
Sun Jan 16 15:53:03 2011 +0100 (2011-01-16)
changeset 41589bbd861837ebc
parent 41588 9546828c0eb3
child 41590 6eeda4b417b3
child 41592 74c0629a11e9
tuned headers;
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Examples.thy
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Hoare_Den.thy
src/HOL/IMP/Hoare_Op.thy
src/HOL/IMP/ROOT.ML
src/HOL/IMP/VC.thy
src/HOL/IMPP/Com.thy
src/HOL/IMPP/EvenOdd.thy
src/HOL/IMPP/Misc.thy
src/HOL/IMPP/Natural.thy
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
src/HOL/Import/Generate-HOL/GenHOL4Word32.thy
src/HOL/Import/Generate-HOL/ROOT.ML
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/Generate-HOLLight/ROOT.ML
src/HOL/Import/HOL/HOL4.thy
src/HOL/Import/HOL4Syntax.thy
src/HOL/Import/HOLLight/ROOT.ML
src/HOL/Import/HOLLightCompat.thy
src/HOL/Import/MakeEqual.thy
src/HOL/Import/mono_scan.ML
src/HOL/Import/mono_seq.ML
src/HOL/MicroJava/Comp/NatCanonify.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/JVM/JVMInstructions.thy
src/HOL/MicroJava/JVM/JVMState.thy
src/HOL/NSA/Filter.thy
src/HOL/NSA/HLim.thy
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Term.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Nominal/Examples/CR.thy
src/HOL/Nominal/Examples/Lambda_mu.thy
src/HOL/Nominal/Examples/Support.thy
src/HOL/Nominal/Examples/VC_Condition.thy
src/HOL/Prolog/ROOT.ML
src/HOL/TLA/Buffer/Buffer.thy
src/HOL/TLA/Buffer/DBuffer.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/MemClerkParameters.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/MemoryParameters.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/TLA/Memory/RPCMemoryParams.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/thry.ML
src/HOL/Tools/TFL/utils.ML
src/HOL/ex/Sudoku.thy
src/HOL/ex/svc_test.thy
     1.1 --- a/src/HOL/IMP/Com.thy	Sun Jan 16 15:31:22 2011 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Sun Jan 16 15:53:03 2011 +0100
     1.3 @@ -1,8 +1,6 @@
     1.4  (*  Title:        HOL/IMP/Com.thy
     1.5 -    ID:           $Id$
     1.6      Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     1.7 -    Isar Version: Gerwin Klein, 2001
     1.8 -    Copyright     1994 TUM
     1.9 +    Author:       Gerwin Klein
    1.10  *)
    1.11  
    1.12  header "Syntax of Commands"
     2.1 --- a/src/HOL/IMP/Denotation.thy	Sun Jan 16 15:31:22 2011 +0100
     2.2 +++ b/src/HOL/IMP/Denotation.thy	Sun Jan 16 15:53:03 2011 +0100
     2.3 @@ -1,7 +1,5 @@
     2.4  (*  Title:      HOL/IMP/Denotation.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     2.7 -    Copyright   1994 TUM
     2.8  *)
     2.9  
    2.10  header "Denotational Semantics of Commands"
     3.1 --- a/src/HOL/IMP/Examples.thy	Sun Jan 16 15:31:22 2011 +0100
     3.2 +++ b/src/HOL/IMP/Examples.thy	Sun Jan 16 15:53:03 2011 +0100
     3.3 @@ -1,7 +1,5 @@
     3.4  (*  Title:      HOL/IMP/Examples.thy
     3.5 -    ID:         $Id$
     3.6      Author:     David von Oheimb, TUM
     3.7 -    Copyright   2000 TUM
     3.8  *)
     3.9  
    3.10  header "Examples"
     4.1 --- a/src/HOL/IMP/Expr.thy	Sun Jan 16 15:31:22 2011 +0100
     4.2 +++ b/src/HOL/IMP/Expr.thy	Sun Jan 16 15:53:03 2011 +0100
     4.3 @@ -1,7 +1,5 @@
     4.4  (*  Title:      HOL/IMP/Expr.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     4.7 -    Copyright   1994 TUM
     4.8  *)
     4.9  
    4.10  header "Expressions"
     5.1 --- a/src/HOL/IMP/Hoare.thy	Sun Jan 16 15:31:22 2011 +0100
     5.2 +++ b/src/HOL/IMP/Hoare.thy	Sun Jan 16 15:53:03 2011 +0100
     5.3 @@ -1,7 +1,5 @@
     5.4  (*  Title:      HOL/IMP/Hoare.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7 -    Copyright   1995 TUM
     5.8  *)
     5.9  
    5.10  header "Inductive Definition of Hoare Logic"
     6.1 --- a/src/HOL/IMP/Hoare_Den.thy	Sun Jan 16 15:31:22 2011 +0100
     6.2 +++ b/src/HOL/IMP/Hoare_Den.thy	Sun Jan 16 15:53:03 2011 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/IMP/Hoare_Def.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Tobias Nipkow
     6.7  *)
     6.8  
     7.1 --- a/src/HOL/IMP/Hoare_Op.thy	Sun Jan 16 15:31:22 2011 +0100
     7.2 +++ b/src/HOL/IMP/Hoare_Op.thy	Sun Jan 16 15:53:03 2011 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/IMP/Hoare_Op.thy
     7.5 -    ID:         $Id$
     7.6      Author:     Tobias Nipkow
     7.7  *)
     7.8  
     8.1 --- a/src/HOL/IMP/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
     8.2 +++ b/src/HOL/IMP/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
     8.3 @@ -1,7 +1,5 @@
     8.4  (*  Title:     HOL/IMP/ROOT.ML
     8.5 -    ID:        $Id$
     8.6      Author:    Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
     8.7 -    Copyright  1995 TUM
     8.8  
     8.9  Caveat: HOLCF/IMP depends on HOL/IMP
    8.10  *)
     9.1 --- a/src/HOL/IMP/VC.thy	Sun Jan 16 15:31:22 2011 +0100
     9.2 +++ b/src/HOL/IMP/VC.thy	Sun Jan 16 15:53:03 2011 +0100
     9.3 @@ -1,7 +1,5 @@
     9.4  (*  Title:      HOL/IMP/VC.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Tobias Nipkow
     9.7 -    Copyright   1996 TUM
     9.8  
     9.9  acom: annotated commands
    9.10  vc:   verification-conditions
    10.1 --- a/src/HOL/IMPP/Com.thy	Sun Jan 16 15:31:22 2011 +0100
    10.2 +++ b/src/HOL/IMPP/Com.thy	Sun Jan 16 15:53:03 2011 +0100
    10.3 @@ -1,7 +1,5 @@
    10.4  (*  Title:    HOL/IMPP/Com.thy
    10.5 -    ID:       $Id$
    10.6      Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
    10.7 -    Copyright 1999 TUM
    10.8  *)
    10.9  
   10.10  header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
    11.1 --- a/src/HOL/IMPP/EvenOdd.thy	Sun Jan 16 15:31:22 2011 +0100
    11.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Sun Jan 16 15:53:03 2011 +0100
    11.3 @@ -1,7 +1,5 @@
    11.4  (*  Title:      HOL/IMPP/EvenOdd.thy
    11.5 -    ID:         $Id$
    11.6 -    Author:     David von Oheimb
    11.7 -    Copyright   1999 TUM
    11.8 +    Author:     David von Oheimb, TUM
    11.9  *)
   11.10  
   11.11  header {* Example of mutually recursive procedures verified with Hoare logic *}
    12.1 --- a/src/HOL/IMPP/Misc.thy	Sun Jan 16 15:31:22 2011 +0100
    12.2 +++ b/src/HOL/IMPP/Misc.thy	Sun Jan 16 15:53:03 2011 +0100
    12.3 @@ -1,7 +1,5 @@
    12.4  (*  Title:      HOL/IMPP/Misc.thy
    12.5 -    ID:         $Id$
    12.6 -    Author:     David von Oheimb
    12.7 -    Copyright   1999 TUM
    12.8 +    Author:     David von Oheimb, TUM
    12.9  *)
   12.10  
   12.11  header {* Several examples for Hoare logic *}
    13.1 --- a/src/HOL/IMPP/Natural.thy	Sun Jan 16 15:31:22 2011 +0100
    13.2 +++ b/src/HOL/IMPP/Natural.thy	Sun Jan 16 15:53:03 2011 +0100
    13.3 @@ -1,7 +1,5 @@
    13.4  (*  Title:      HOL/IMPP/Natural.thy
    13.5 -    ID:         $Id$
    13.6      Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
    13.7 -    Copyright   1999 TUM
    13.8  *)
    13.9  
   13.10  header {* Natural semantics of commands *}
    14.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sun Jan 16 15:31:22 2011 +0100
    14.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sun Jan 16 15:53:03 2011 +0100
    14.3 @@ -1,6 +1,5 @@
    14.4  (*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
    14.5 -    ID:         $Id$
    14.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    14.7 +    Author:     Sebastian Skalberg, TU Muenchen
    14.8  *)
    14.9  
   14.10  theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;
    15.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sun Jan 16 15:31:22 2011 +0100
    15.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sun Jan 16 15:53:03 2011 +0100
    15.3 @@ -1,6 +1,5 @@
    15.4  (*  Title:      HOL/Import/Generate-HOL/GenHOL4Prob.thy
    15.5 -    ID:         $Id$
    15.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    15.7 +    Author:     Sebastian Skalberg, TU Muenchen
    15.8  *)
    15.9  
   15.10  theory GenHOL4Prob imports GenHOL4Real begin
    16.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sun Jan 16 15:31:22 2011 +0100
    16.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sun Jan 16 15:53:03 2011 +0100
    16.3 @@ -1,6 +1,5 @@
    16.4  (*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
    16.5 -    ID:         $Id$
    16.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    16.7 +    Author:     Sebastian Skalberg, TU Muenchen
    16.8  *)
    16.9  
   16.10  theory GenHOL4Vec imports GenHOL4Base begin
    17.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sun Jan 16 15:31:22 2011 +0100
    17.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sun Jan 16 15:53:03 2011 +0100
    17.3 @@ -1,6 +1,5 @@
    17.4  (*  Title:      HOL/Import/Generate-HOL/GenHOL4Word32.thy
    17.5 -    ID:         $Id$
    17.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    17.7 +    Author:     Sebastian Skalberg, TU Muenchen
    17.8  *)
    17.9  
   17.10  theory GenHOL4Word32 imports GenHOL4Base begin;
    18.1 --- a/src/HOL/Import/Generate-HOL/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
    18.2 +++ b/src/HOL/Import/Generate-HOL/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
    18.3 @@ -1,8 +1,3 @@
    18.4 -(*  Title:      HOL/Import/Generate-HOL/ROOT.ML
    18.5 -    ID:         $Id$
    18.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    18.7 -*)
    18.8 -
    18.9  use_thy "GenHOL4Prob";
   18.10  use_thy "GenHOL4Vec";
   18.11  use_thy "GenHOL4Word32";
    19.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sun Jan 16 15:31:22 2011 +0100
    19.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sun Jan 16 15:53:03 2011 +0100
    19.3 @@ -1,6 +1,5 @@
    19.4  (*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
    19.5 -    ID:         $Id$
    19.6 -    Author:     Steven Obua (TU Muenchen)
    19.7 +    Author:     Steven Obua, TU Muenchen
    19.8  *)
    19.9  
   19.10  theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
    20.1 --- a/src/HOL/Import/Generate-HOLLight/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
    20.2 +++ b/src/HOL/Import/Generate-HOLLight/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
    20.3 @@ -1,6 +1,1 @@
    20.4 -(*  Title:      HOL/Import/Generate-HOLLight/ROOT.ML
    20.5 -    ID:         $Id$
    20.6 -    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
    20.7 -*)
    20.8 -
    20.9  use_thy "GenHOLLight";
    21.1 --- a/src/HOL/Import/HOL/HOL4.thy	Sun Jan 16 15:31:22 2011 +0100
    21.2 +++ b/src/HOL/Import/HOL/HOL4.thy	Sun Jan 16 15:53:03 2011 +0100
    21.3 @@ -1,6 +1,5 @@
    21.4  (*  Title:      HOL/Import/HOL/HOL4.thy
    21.5 -    ID:         $Id$
    21.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    21.7 +    Author:     Sebastian Skalberg, TU Muenchen
    21.8  *)
    21.9  
   21.10  theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin
    22.1 --- a/src/HOL/Import/HOL4Syntax.thy	Sun Jan 16 15:31:22 2011 +0100
    22.2 +++ b/src/HOL/Import/HOL4Syntax.thy	Sun Jan 16 15:53:03 2011 +0100
    22.3 @@ -1,10 +1,11 @@
    22.4  (*  Title:      HOL/Import/HOL4Syntax.thy
    22.5 -    ID:         $Id$
    22.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    22.7 +    Author:     Sebastian Skalberg, TU Muenchen
    22.8  *)
    22.9  
   22.10 -theory HOL4Syntax imports HOL4Setup
   22.11 -  uses "import_syntax.ML" begin
   22.12 +theory HOL4Syntax
   22.13 +imports HOL4Setup
   22.14 +uses "import_syntax.ML"
   22.15 +begin
   22.16  
   22.17  ML {* HOL4ImportSyntax.setup() *}
   22.18  
    23.1 --- a/src/HOL/Import/HOLLight/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
    23.2 +++ b/src/HOL/Import/HOLLight/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
    23.3 @@ -1,5 +1,1 @@
    23.4 -(*  Title:      HOL/Import/HOLLight/ROOT.ML
    23.5 -    ID:         $Id$
    23.6 -*)
    23.7 -
    23.8  use_thy "HOLLight";
    24.1 --- a/src/HOL/Import/HOLLightCompat.thy	Sun Jan 16 15:31:22 2011 +0100
    24.2 +++ b/src/HOL/Import/HOLLightCompat.thy	Sun Jan 16 15:53:03 2011 +0100
    24.3 @@ -1,6 +1,5 @@
    24.4  (*  Title:      HOL/Import/HOLLightCompat.thy
    24.5 -    ID:         $Id$
    24.6 -    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
    24.7 +    Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
    24.8  *)
    24.9  
   24.10  theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
    25.1 --- a/src/HOL/Import/MakeEqual.thy	Sun Jan 16 15:31:22 2011 +0100
    25.2 +++ b/src/HOL/Import/MakeEqual.thy	Sun Jan 16 15:53:03 2011 +0100
    25.3 @@ -1,6 +1,5 @@
    25.4  (*  Title:      HOL/Import/MakeEqual.thy
    25.5 -    ID:         $Id$
    25.6 -    Author:     Sebastian Skalberg (TU Muenchen)
    25.7 +    Author:     Sebastian Skalberg, TU Muenchen
    25.8  *)
    25.9  
   25.10  theory MakeEqual imports Main
    26.1 --- a/src/HOL/Import/mono_scan.ML	Sun Jan 16 15:31:22 2011 +0100
    26.2 +++ b/src/HOL/Import/mono_scan.ML	Sun Jan 16 15:53:03 2011 +0100
    26.3 @@ -1,8 +1,7 @@
    26.4  (*  Title:      HOL/Import/mono_scan.ML
    26.5 -    ID:         $Id$
    26.6      Author:     Steven Obua, TU Muenchen
    26.7  
    26.8 -    Monomorphic scanner combinators for monomorphic sequences.
    26.9 +Monomorphic scanner combinators for monomorphic sequences.
   26.10  *)
   26.11  
   26.12  signature MONO_SCANNER =
    27.1 --- a/src/HOL/Import/mono_seq.ML	Sun Jan 16 15:31:22 2011 +0100
    27.2 +++ b/src/HOL/Import/mono_seq.ML	Sun Jan 16 15:53:03 2011 +0100
    27.3 @@ -1,8 +1,7 @@
    27.4  (*  Title:      HOL/Import/mono_seq.ML
    27.5 -    ID:         $Id$
    27.6      Author:     Steven Obua, TU Muenchen
    27.7  
    27.8 -    Monomorphic sequences.
    27.9 +Monomorphic sequences.
   27.10  *)
   27.11  
   27.12  (* The trouble is that signature / structures cannot depend on type variable parameters ... *)
    28.1 --- a/src/HOL/MicroJava/Comp/NatCanonify.thy	Sun Jan 16 15:31:22 2011 +0100
    28.2 +++ b/src/HOL/MicroJava/Comp/NatCanonify.thy	Sun Jan 16 15:53:03 2011 +0100
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      HOL/MicroJava/Comp/NatCanonify.thy
    28.5 -    ID:         $Id$
    28.6      Author:     Martin Strecker
    28.7  *)
    28.8  
    29.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Sun Jan 16 15:31:22 2011 +0100
    29.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Sun Jan 16 15:53:03 2011 +0100
    29.3 @@ -1,7 +1,5 @@
    29.4  (*  Title:      HOL/MicroJava/J/JBasis.thy
    29.5 -    ID:         $Id$
    29.6 -    Author:     David von Oheimb
    29.7 -    Copyright   1999 TU Muenchen
    29.8 +    Author:     David von Oheimb, TU Muenchen
    29.9  *)
   29.10  
   29.11  header {* 
    30.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Jan 16 15:31:22 2011 +0100
    30.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Jan 16 15:53:03 2011 +0100
    30.3 @@ -1,7 +1,5 @@
    30.4  (*  Title:      HOL/MicroJava/J/JTypeSafe.thy
    30.5 -    ID:         $Id$
    30.6 -    Author:     David von Oheimb
    30.7 -    Copyright   1999 Technische Universitaet Muenchen
    30.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    30.9  *)
   30.10  
   30.11  header {* \isaheader{Type Safety Proof} *}
    31.1 --- a/src/HOL/MicroJava/J/Term.thy	Sun Jan 16 15:31:22 2011 +0100
    31.2 +++ b/src/HOL/MicroJava/J/Term.thy	Sun Jan 16 15:53:03 2011 +0100
    31.3 @@ -1,7 +1,5 @@
    31.4  (*  Title:      HOL/MicroJava/J/Term.thy
    31.5 -    ID:         $Id$
    31.6 -    Author:     David von Oheimb
    31.7 -    Copyright   1999 Technische Universitaet Muenchen
    31.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    31.9  *)
   31.10  
   31.11  header {* \isaheader{Expressions and Statements} *}
    32.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Sun Jan 16 15:31:22 2011 +0100
    32.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Sun Jan 16 15:53:03 2011 +0100
    32.3 @@ -1,7 +1,5 @@
    32.4  (*  Title:      HOL/MicroJava/J/TypeRel.thy
    32.5 -    ID:         $Id$
    32.6 -    Author:     David von Oheimb
    32.7 -    Copyright   1999 Technische Universitaet Muenchen
    32.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    32.9  *)
   32.10  
   32.11  header {* \isaheader{Relations between Java Types} *}
    33.1 --- a/src/HOL/MicroJava/J/Value.thy	Sun Jan 16 15:31:22 2011 +0100
    33.2 +++ b/src/HOL/MicroJava/J/Value.thy	Sun Jan 16 15:53:03 2011 +0100
    33.3 @@ -1,7 +1,5 @@
    33.4  (*  Title:      HOL/MicroJava/J/Value.thy
    33.5 -    ID:         $Id$
    33.6 -    Author:     David von Oheimb
    33.7 -    Copyright   1999 Technische Universitaet Muenchen
    33.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    33.9  *)
   33.10  
   33.11  header {* \isaheader{Java Values} *}
    34.1 --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Jan 16 15:31:22 2011 +0100
    34.2 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Jan 16 15:53:03 2011 +0100
    34.3 @@ -1,7 +1,5 @@
    34.4  (*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
    34.5 -    ID:         $Id$
    34.6 -    Author:     Gerwin Klein
    34.7 -    Copyright   2000 Technische Universitaet Muenchen
    34.8 +    Author:     Gerwin Klein, Technische Universitaet Muenchen
    34.9  *)
   34.10  
   34.11  header {* \isaheader{Instructions of the JVM} *}
    35.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Sun Jan 16 15:31:22 2011 +0100
    35.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sun Jan 16 15:53:03 2011 +0100
    35.3 @@ -1,7 +1,5 @@
    35.4  (*  Title:      HOL/MicroJava/JVM/JVMState.thy
    35.5 -    ID:         $Id$
    35.6 -    Author:     Cornelia Pusch, Gerwin Klein
    35.7 -    Copyright   1999 Technische Universitaet Muenchen
    35.8 +    Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
    35.9  *)
   35.10  
   35.11  header {* 
    36.1 --- a/src/HOL/NSA/Filter.thy	Sun Jan 16 15:31:22 2011 +0100
    36.2 +++ b/src/HOL/NSA/Filter.thy	Sun Jan 16 15:53:03 2011 +0100
    36.3 @@ -1,9 +1,7 @@
    36.4 -(*  Title       : Filter.thy
    36.5 -    ID          : $Id$
    36.6 -    Author      : Jacques D. Fleuriot
    36.7 -    Copyright   : 1998  University of Cambridge
    36.8 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    36.9 -    Conversion to locales by Brian Huffman, 2005
   36.10 +(*  Title:      Filter.thy
   36.11 +    Author:     Jacques D. Fleuriot, University of Cambridge
   36.12 +    Author:     Lawrence C Paulson
   36.13 +    Author:     Brian Huffman
   36.14  *) 
   36.15  
   36.16  header {* Filters and Ultrafilters *}
    37.1 --- a/src/HOL/NSA/HLim.thy	Sun Jan 16 15:31:22 2011 +0100
    37.2 +++ b/src/HOL/NSA/HLim.thy	Sun Jan 16 15:53:03 2011 +0100
    37.3 @@ -1,8 +1,6 @@
    37.4 -(*  Title       : HLim.thy
    37.5 -    ID          : $Id$
    37.6 -    Author      : Jacques D. Fleuriot
    37.7 -    Copyright   : 1998  University of Cambridge
    37.8 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    37.9 +(*  Title:      HLim.thy
   37.10 +    Author:     Jacques D. Fleuriot, University of Cambridge
   37.11 +    Author:     Lawrence C Paulson
   37.12  *)
   37.13  
   37.14  header{* Limits and Continuity (Nonstandard) *}
    38.1 --- a/src/HOL/NanoJava/AxSem.thy	Sun Jan 16 15:31:22 2011 +0100
    38.2 +++ b/src/HOL/NanoJava/AxSem.thy	Sun Jan 16 15:53:03 2011 +0100
    38.3 @@ -1,7 +1,5 @@
    38.4  (*  Title:      HOL/NanoJava/AxSem.thy
    38.5 -    ID:         $Id$
    38.6 -    Author:     David von Oheimb
    38.7 -    Copyright   2001 Technische Universitaet Muenchen
    38.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    38.9  *)
   38.10  
   38.11  header "Axiomatic Semantics"
    39.1 --- a/src/HOL/NanoJava/Term.thy	Sun Jan 16 15:31:22 2011 +0100
    39.2 +++ b/src/HOL/NanoJava/Term.thy	Sun Jan 16 15:53:03 2011 +0100
    39.3 @@ -1,7 +1,5 @@
    39.4  (*  Title:      HOL/NanoJava/Term.thy
    39.5 -    ID:         $Id$
    39.6 -    Author:     David von Oheimb
    39.7 -    Copyright   2001 Technische Universitaet Muenchen
    39.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    39.9  *)
   39.10  
   39.11  header "Statements and expression emulations"
    40.1 --- a/src/HOL/NanoJava/TypeRel.thy	Sun Jan 16 15:31:22 2011 +0100
    40.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Sun Jan 16 15:53:03 2011 +0100
    40.3 @@ -1,7 +1,5 @@
    40.4  (*  Title:      HOL/NanoJava/TypeRel.thy
    40.5 -    ID:         $Id$
    40.6 -    Author:     David von Oheimb
    40.7 -    Copyright   2001 Technische Universitaet Muenchen
    40.8 +    Author:     David von Oheimb, Technische Universitaet Muenchen
    40.9  *)
   40.10  
   40.11  header "Type relations"
    41.1 --- a/src/HOL/Nominal/Examples/CR.thy	Sun Jan 16 15:31:22 2011 +0100
    41.2 +++ b/src/HOL/Nominal/Examples/CR.thy	Sun Jan 16 15:53:03 2011 +0100
    41.3 @@ -1,5 +1,3 @@
    41.4 -(* $Id$ *)
    41.5 -
    41.6  theory CR
    41.7  imports Lam_Funs
    41.8  begin
    42.1 --- a/src/HOL/Nominal/Examples/Lambda_mu.thy	Sun Jan 16 15:31:22 2011 +0100
    42.2 +++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Sun Jan 16 15:53:03 2011 +0100
    42.3 @@ -1,5 +1,3 @@
    42.4 -(* $Id$ *)
    42.5 -
    42.6  theory Lambda_mu 
    42.7    imports "../Nominal" 
    42.8  begin
    43.1 --- a/src/HOL/Nominal/Examples/Support.thy	Sun Jan 16 15:31:22 2011 +0100
    43.2 +++ b/src/HOL/Nominal/Examples/Support.thy	Sun Jan 16 15:53:03 2011 +0100
    43.3 @@ -1,5 +1,3 @@
    43.4 -(* $Id$ *)
    43.5 -
    43.6  theory Support 
    43.7    imports "../Nominal" 
    43.8  begin
    44.1 --- a/src/HOL/Nominal/Examples/VC_Condition.thy	Sun Jan 16 15:31:22 2011 +0100
    44.2 +++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Sun Jan 16 15:53:03 2011 +0100
    44.3 @@ -1,5 +1,3 @@
    44.4 -(* $Id$ *)
    44.5 -
    44.6  theory VC_Condition
    44.7  imports "../Nominal" 
    44.8  begin
    45.1 --- a/src/HOL/Prolog/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
    45.2 +++ b/src/HOL/Prolog/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:    HOL/Prolog/ROOT.ML
    45.5 -    ID:       $Id$
    45.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    45.7  *)
    45.8  
    46.1 --- a/src/HOL/TLA/Buffer/Buffer.thy	Sun Jan 16 15:31:22 2011 +0100
    46.2 +++ b/src/HOL/TLA/Buffer/Buffer.thy	Sun Jan 16 15:53:03 2011 +0100
    46.3 @@ -1,8 +1,5 @@
    46.4 -(*
    46.5 -    File:        Buffer.thy
    46.6 -    ID:          $Id$
    46.7 -    Author:      Stephan Merz
    46.8 -    Copyright:   1997 University of Munich
    46.9 +(*  Title:      HOL/TLA/Buffer/Buffer.thy
   46.10 +    Author:     Stephan Merz, University of Munich
   46.11  *)
   46.12  
   46.13  header {* A simple FIFO buffer (synchronous communication, interleaving) *}
    47.1 --- a/src/HOL/TLA/Buffer/DBuffer.thy	Sun Jan 16 15:31:22 2011 +0100
    47.2 +++ b/src/HOL/TLA/Buffer/DBuffer.thy	Sun Jan 16 15:53:03 2011 +0100
    47.3 @@ -1,8 +1,5 @@
    47.4 -(*
    47.5 -    File:        DBuffer.thy
    47.6 -    ID:          $Id$
    47.7 -    Author:      Stephan Merz
    47.8 -    Copyright:   1997 University of Munich
    47.9 +(*  Title:      HOL/TLA/Buffer/DBuffer.thy
   47.10 +    Author:     Stephan Merz, University of Munich
   47.11  *)
   47.12  
   47.13  header {* Two FIFO buffers in a row, with interleaving assumption *}
    48.1 --- a/src/HOL/TLA/Inc/Inc.thy	Sun Jan 16 15:31:22 2011 +0100
    48.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Sun Jan 16 15:53:03 2011 +0100
    48.3 @@ -1,8 +1,5 @@
    48.4 -(*
    48.5 -    File:        TLA/Inc/Inc.thy
    48.6 -    ID:          $Id$
    48.7 -    Author:      Stephan Merz
    48.8 -    Copyright:   1997 University of Munich
    48.9 +(*  Title:      HOL/TLA/Inc/Inc.thy
   48.10 +    Author:     Stephan Merz, University of Munich
   48.11  *)
   48.12  
   48.13  header {* Lamport's "increment" example *}
    49.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Sun Jan 16 15:31:22 2011 +0100
    49.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Sun Jan 16 15:53:03 2011 +0100
    49.3 @@ -1,8 +1,5 @@
    49.4 -(*
    49.5 -    File:        MemClerk.thy
    49.6 -    ID:          $Id$
    49.7 -    Author:      Stephan Merz
    49.8 -    Copyright:   1997 University of Munich
    49.9 +(*  Title:      HOL/TLA/Memory/MemClerk.thy
   49.10 +    Author:     Stephan Merz, University of Munich
   49.11  *)
   49.12  
   49.13  header {* RPC-Memory example: specification of the memory clerk *}
    50.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Jan 16 15:31:22 2011 +0100
    50.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Jan 16 15:53:03 2011 +0100
    50.3 @@ -1,8 +1,5 @@
    50.4 -(*
    50.5 -    File:        MemClerkParameters.thy
    50.6 -    ID:          $Id$
    50.7 -    Author:      Stephan Merz
    50.8 -    Copyright:   1997 University of Munich
    50.9 +(*  Title:      HOL/TLA/Memory/MemClerkParameters.thy
   50.10 +    Author:     Stephan Merz, University of Munich
   50.11  *)
   50.12  
   50.13  header {* RPC-Memory example: Parameters of the memory clerk *}
    51.1 --- a/src/HOL/TLA/Memory/Memory.thy	Sun Jan 16 15:31:22 2011 +0100
    51.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Sun Jan 16 15:53:03 2011 +0100
    51.3 @@ -1,8 +1,5 @@
    51.4 -(*
    51.5 -    File:        Memory.thy
    51.6 -    ID:          $Id$
    51.7 -    Author:      Stephan Merz
    51.8 -    Copyright:   1997 University of Munich
    51.9 +(*  Title:      HOL/TLA/Memory/Memory.thy
   51.10 +    Author:     Stephan Merz, University of Munich
   51.11  *)
   51.12  
   51.13  header {* RPC-Memory example: Memory specification *}
    52.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Jan 16 15:31:22 2011 +0100
    52.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Jan 16 15:53:03 2011 +0100
    52.3 @@ -1,8 +1,5 @@
    52.4 -(*
    52.5 -    File:        MemoryImplementation.thy
    52.6 -    ID:          $Id$
    52.7 -    Author:      Stephan Merz
    52.8 -    Copyright:   1997 University of Munich
    52.9 +(*  Title:      HOL/TLA/Memory/MemoryImplementation.thy
   52.10 +    Author:     Stephan Merz, University of Munich
   52.11  *)
   52.12  
   52.13  header {* RPC-Memory example: Memory implementation *}
    53.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Sun Jan 16 15:31:22 2011 +0100
    53.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Sun Jan 16 15:53:03 2011 +0100
    53.3 @@ -1,8 +1,5 @@
    53.4 -(*
    53.5 -    File:        MemoryParameters.thy
    53.6 -    ID:          $Id$
    53.7 -    Author:      Stephan Merz
    53.8 -    Copyright:   1997 University of Munich
    53.9 +(*  Title:      HOL/TLA/Memory/MemoryParameters.thy
   53.10 +    Author:     Stephan Merz, University of Munich
   53.11  *)
   53.12  
   53.13  header {* RPC-Memory example: Memory parameters *}
    54.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Jan 16 15:31:22 2011 +0100
    54.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Jan 16 15:53:03 2011 +0100
    54.3 @@ -1,8 +1,5 @@
    54.4 -(*
    54.5 -    File:        ProcedureInterface.thy
    54.6 -    ID:          $Id$
    54.7 -    Author:      Stephan Merz
    54.8 -    Copyright:   1997 University of Munich
    54.9 +(*  Title:      HOL/TLA/Memory/ProcedureInterface.thy
   54.10 +    Author:     Stephan Merz, University of Munich
   54.11  *)
   54.12  
   54.13  header {* Procedure interface for RPC-Memory components *}
    55.1 --- a/src/HOL/TLA/Memory/RPC.thy	Sun Jan 16 15:31:22 2011 +0100
    55.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Sun Jan 16 15:53:03 2011 +0100
    55.3 @@ -1,8 +1,5 @@
    55.4 -(*
    55.5 -    File:        RPC.thy
    55.6 -    ID:          $Id$
    55.7 -    Author:      Stephan Merz
    55.8 -    Copyright:   1997 University of Munich
    55.9 +(*  Title:      HOL/TLA/Memory/RPC.thy
   55.10 +    Author:     Stephan Merz, University of Munich
   55.11  *)
   55.12  
   55.13  header {* RPC-Memory example: RPC specification *}
    56.1 --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Jan 16 15:31:22 2011 +0100
    56.2 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Jan 16 15:53:03 2011 +0100
    56.3 @@ -1,8 +1,5 @@
    56.4 -(*
    56.5 -    File:        RPCMemoryParams.thy
    56.6 -    ID:          $Id$
    56.7 -    Author:      Stephan Merz
    56.8 -    Copyright:   1997 University of Munich
    56.9 +(*  Title:      HOL/TLA/Memory/RPCMemoryParams.thy
   56.10 +    Author:     Stephan Merz, University of Munich
   56.11  *)
   56.12  
   56.13  header {* Basic declarations for the RPC-memory example *}
    57.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Sun Jan 16 15:31:22 2011 +0100
    57.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Sun Jan 16 15:53:03 2011 +0100
    57.3 @@ -1,8 +1,5 @@
    57.4 -(*
    57.5 -    File:        RPCParameters.thy
    57.6 -    ID:          $Id$
    57.7 -    Author:      Stephan Merz
    57.8 -    Copyright:   1997 University of Munich
    57.9 +(*  Title:      HOL/TLA/Memory/RPCParameters.thy
   57.10 +    Author:     Stephan Merz, University of Munich
   57.11  *)
   57.12  
   57.13  header {* RPC-Memory example: RPC parameters *}
    58.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Sun Jan 16 15:31:22 2011 +0100
    58.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Sun Jan 16 15:53:03 2011 +0100
    58.3 @@ -1,7 +1,5 @@
    58.4  (*  Title:      HOL/Tools/TFL/dcterm.ML
    58.5 -    ID:         $Id$
    58.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    58.7 -    Copyright   1997  University of Cambridge
    58.8  *)
    58.9  
   58.10  (*---------------------------------------------------------------------------
    59.1 --- a/src/HOL/Tools/TFL/thry.ML	Sun Jan 16 15:31:22 2011 +0100
    59.2 +++ b/src/HOL/Tools/TFL/thry.ML	Sun Jan 16 15:53:03 2011 +0100
    59.3 @@ -1,7 +1,5 @@
    59.4  (*  Title:      HOL/Tools/TFL/thry.ML
    59.5 -    ID:         $Id$
    59.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    59.7 -    Copyright   1997  University of Cambridge
    59.8  *)
    59.9  
   59.10  signature THRY =
    60.1 --- a/src/HOL/Tools/TFL/utils.ML	Sun Jan 16 15:31:22 2011 +0100
    60.2 +++ b/src/HOL/Tools/TFL/utils.ML	Sun Jan 16 15:53:03 2011 +0100
    60.3 @@ -1,7 +1,5 @@
    60.4  (*  Title:      HOL/Tools/TFL/utils.ML
    60.5 -    ID:         $Id$
    60.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    60.7 -    Copyright   1997  University of Cambridge
    60.8  
    60.9  Basic utilities.
   60.10  *)
    61.1 --- a/src/HOL/ex/Sudoku.thy	Sun Jan 16 15:31:22 2011 +0100
    61.2 +++ b/src/HOL/ex/Sudoku.thy	Sun Jan 16 15:53:03 2011 +0100
    61.3 @@ -1,5 +1,4 @@
    61.4 -(*  Title:      Sudoku.thy
    61.5 -    ID:         $Id$
    61.6 +(*  Title:      HOL/ex/Sudoku.thy
    61.7      Author:     Tjark Weber
    61.8      Copyright   2005-2008
    61.9  *)
    62.1 --- a/src/HOL/ex/svc_test.thy	Sun Jan 16 15:31:22 2011 +0100
    62.2 +++ b/src/HOL/ex/svc_test.thy	Sun Jan 16 15:53:03 2011 +0100
    62.3 @@ -1,6 +1,3 @@
    62.4 -
    62.5 -(* $Id$ *)
    62.6 -
    62.7  header {* Demonstrating the interface SVC *}
    62.8  
    62.9  theory svc_test