# HG changeset patch
# User wenzelm
# Date 1295189583 -3600
# Node ID bbd861837ebc01b29283130e5605961f4beb7c54
# Parent  9546828c0eb3ec2c9b4ae234efa491b95ce01dc6
tuned headers;

diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Com.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,6 @@
 (*  Title:        HOL/IMP/Com.thy
-    ID:           $Id$
     Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-    Isar Version: Gerwin Klein, 2001
-    Copyright     1994 TUM
+    Author:       Gerwin Klein
 *)
 
 header "Syntax of Commands"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Denotation.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMP/Denotation.thy
-    ID:         $Id$
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
 *)
 
 header "Denotational Semantics of Commands"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Examples.thy
--- a/src/HOL/IMP/Examples.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Examples.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMP/Examples.thy
-    ID:         $Id$
     Author:     David von Oheimb, TUM
-    Copyright   2000 TUM
 *)
 
 header "Examples"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Expr.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMP/Expr.thy
-    ID:         $Id$
     Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-    Copyright   1994 TUM
 *)
 
 header "Expressions"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Hoare.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMP/Hoare.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1995 TUM
 *)
 
 header "Inductive Definition of Hoare Logic"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Hoare_Den.thy
--- a/src/HOL/IMP/Hoare_Den.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Hoare_Den.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/IMP/Hoare_Def.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
 *)
 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/Hoare_Op.thy
--- a/src/HOL/IMP/Hoare_Op.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/Hoare_Op.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/IMP/Hoare_Op.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
 *)
 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:     HOL/IMP/ROOT.ML
-    ID:        $Id$
     Author:    Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
-    Copyright  1995 TUM
 
 Caveat: HOLCF/IMP depends on HOL/IMP
 *)
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMP/VC.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMP/VC.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1996 TUM
 
 acom: annotated commands
 vc:   verification-conditions
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/Com.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:    HOL/IMPP/Com.thy
-    ID:       $Id$
     Author:   David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
-    Copyright 1999 TUM
 *)
 
 header {* Semantics of arithmetic and boolean expressions, Syntax of commands *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMPP/EvenOdd.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 TUM
+    Author:     David von Oheimb, TUM
 *)
 
 header {* Example of mutually recursive procedures verified with Hoare logic *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMPP/Misc.thy
--- a/src/HOL/IMPP/Misc.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/Misc.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMPP/Misc.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 TUM
+    Author:     David von Oheimb, TUM
 *)
 
 header {* Several examples for Hoare logic *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/IMPP/Natural.thy
--- a/src/HOL/IMPP/Natural.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/IMPP/Natural.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/IMPP/Natural.thy
-    ID:         $Id$
     Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
-    Copyright   1999 TUM
 *)
 
 header {* Natural semantics of commands *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
 theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/Generate-HOL/GenHOL4Prob.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
 theory GenHOL4Prob imports GenHOL4Real begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
 theory GenHOL4Vec imports GenHOL4Base begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOL/GenHOL4Word32.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/Generate-HOL/GenHOL4Word32.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
 theory GenHOL4Word32 imports GenHOL4Base begin;
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOL/ROOT.ML
--- a/src/HOL/Import/Generate-HOL/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOL/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,3 @@
-(*  Title:      HOL/Import/Generate-HOL/ROOT.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-*)
-
 use_thy "GenHOL4Prob";
 use_thy "GenHOL4Vec";
 use_thy "GenHOL4Word32";
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/Generate-HOLLight/GenHOLLight.thy
-    ID:         $Id$
-    Author:     Steven Obua (TU Muenchen)
+    Author:     Steven Obua, TU Muenchen
 *)
 
 theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin;
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/Generate-HOLLight/ROOT.ML
--- a/src/HOL/Import/Generate-HOLLight/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/Generate-HOLLight/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,1 @@
-(*  Title:      HOL/Import/Generate-HOLLight/ROOT.ML
-    ID:         $Id$
-    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
-*)
-
 use_thy "GenHOLLight";
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/HOL/HOL4.thy
--- a/src/HOL/Import/HOL/HOL4.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOL/HOL4.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/HOL/HOL4.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
 theory HOL4 imports HOL4Vec HOL4Word32 HOL4Real begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/HOL4Syntax.thy
--- a/src/HOL/Import/HOL4Syntax.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOL4Syntax.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,10 +1,11 @@
 (*  Title:      HOL/Import/HOL4Syntax.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
-theory HOL4Syntax imports HOL4Setup
-  uses "import_syntax.ML" begin
+theory HOL4Syntax
+imports HOL4Setup
+uses "import_syntax.ML"
+begin
 
 ML {* HOL4ImportSyntax.setup() *}
 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/HOLLight/ROOT.ML
--- a/src/HOL/Import/HOLLight/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOLLight/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,1 @@
-(*  Title:      HOL/Import/HOLLight/ROOT.ML
-    ID:         $Id$
-*)
-
 use_thy "HOLLight";
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/HOLLightCompat.thy
--- a/src/HOL/Import/HOLLightCompat.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/HOLLightCompat.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/HOLLightCompat.thy
-    ID:         $Id$
-    Author:     Steven Obua and Sebastian Skalberg (TU Muenchen)
+    Author:     Steven Obua and Sebastian Skalberg, TU Muenchen
 *)
 
 theory HOLLightCompat imports HOL4Setup HOL4Compat Divides Primes Real begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/MakeEqual.thy
--- a/src/HOL/Import/MakeEqual.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/MakeEqual.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/MakeEqual.thy
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
+    Author:     Sebastian Skalberg, TU Muenchen
 *)
 
 theory MakeEqual imports Main
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/mono_scan.ML
--- a/src/HOL/Import/mono_scan.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/mono_scan.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOL/Import/mono_scan.ML
-    ID:         $Id$
     Author:     Steven Obua, TU Muenchen
 
-    Monomorphic scanner combinators for monomorphic sequences.
+Monomorphic scanner combinators for monomorphic sequences.
 *)
 
 signature MONO_SCANNER =
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Import/mono_seq.ML
--- a/src/HOL/Import/mono_seq.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Import/mono_seq.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,7 @@
 (*  Title:      HOL/Import/mono_seq.ML
-    ID:         $Id$
     Author:     Steven Obua, TU Muenchen
 
-    Monomorphic sequences.
+Monomorphic sequences.
 *)
 
 (* The trouble is that signature / structures cannot depend on type variable parameters ... *)
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/Comp/NatCanonify.thy
--- a/src/HOL/MicroJava/Comp/NatCanonify.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/Comp/NatCanonify.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/Comp/NatCanonify.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/J/JBasis.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
 header {* 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/J/JTypeSafe.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Type Safety Proof} *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/J/Term.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Expressions and Statements} *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/J/TypeRel.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Relations between Java Types} *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/J/Value.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/J/Value.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Java Values} *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
-    ID:         $Id$
-    Author:     Gerwin Klein
-    Copyright   2000 Technische Universitaet Muenchen
+    Author:     Gerwin Klein, Technische Universitaet Muenchen
 *)
 
 header {* \isaheader{Instructions of the JVM} *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/MicroJava/JVM/JVMState.thy
-    ID:         $Id$
-    Author:     Cornelia Pusch, Gerwin Klein
-    Copyright   1999 Technische Universitaet Muenchen
+    Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
 *)
 
 header {* 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NSA/Filter.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,9 +1,7 @@
-(*  Title       : Filter.thy
-    ID          : $Id$
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
-    Conversion to locales by Brian Huffman, 2005
+(*  Title:      Filter.thy
+    Author:     Jacques D. Fleuriot, University of Cambridge
+    Author:     Lawrence C Paulson
+    Author:     Brian Huffman
 *) 
 
 header {* Filters and Ultrafilters *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NSA/HLim.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,6 @@
-(*  Title       : HLim.thy
-    ID          : $Id$
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+(*  Title:      HLim.thy
+    Author:     Jacques D. Fleuriot, University of Cambridge
+    Author:     Lawrence C Paulson
 *)
 
 header{* Limits and Continuity (Nonstandard) *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/NanoJava/AxSem.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   2001 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header "Axiomatic Semantics"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NanoJava/Term.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/NanoJava/Term.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   2001 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header "Statements and expression emulations"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/NanoJava/TypeRel.thy
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   2001 Technische Universitaet Muenchen
+    Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
 header "Type relations"
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory CR
 imports Lam_Funs
 begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Nominal/Examples/Lambda_mu.thy
--- a/src/HOL/Nominal/Examples/Lambda_mu.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Lambda_mu 
   imports "../Nominal" 
 begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Nominal/Examples/Support.thy
--- a/src/HOL/Nominal/Examples/Support.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Support 
   imports "../Nominal" 
 begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory VC_Condition
 imports "../Nominal" 
 begin
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Prolog/ROOT.ML
--- a/src/HOL/Prolog/ROOT.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Prolog/ROOT.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
 (*  Title:    HOL/Prolog/ROOT.ML
-    ID:       $Id$
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        Buffer.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Buffer/Buffer.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* A simple FIFO buffer (synchronous communication, interleaving) *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Buffer/DBuffer.thy
--- a/src/HOL/TLA/Buffer/DBuffer.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Buffer/DBuffer.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        DBuffer.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Buffer/DBuffer.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* Two FIFO buffers in a row, with interleaving assumption *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Inc/Inc.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        TLA/Inc/Inc.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Inc/Inc.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* Lamport's "increment" example *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        MemClerk.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/MemClerk.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: specification of the memory clerk *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/MemClerkParameters.thy
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        MemClerkParameters.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/MemClerkParameters.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: Parameters of the memory clerk *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        Memory.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/Memory.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: Memory specification *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        MemoryImplementation.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/MemoryImplementation.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: Memory implementation *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/MemoryParameters.thy
--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        MemoryParameters.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/MemoryParameters.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: Memory parameters *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        ProcedureInterface.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/ProcedureInterface.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* Procedure interface for RPC-Memory components *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        RPC.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/RPC.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: RPC specification *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/RPCMemoryParams.thy
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        RPCMemoryParams.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/RPCMemoryParams.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* Basic declarations for the RPC-memory example *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/TLA/Memory/RPCParameters.thy
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,8 +1,5 @@
-(*
-    File:        RPCParameters.thy
-    ID:          $Id$
-    Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+(*  Title:      HOL/TLA/Memory/RPCParameters.thy
+    Author:     Stephan Merz, University of Munich
 *)
 
 header {* RPC-Memory example: RPC parameters *}
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Tools/TFL/dcterm.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 *)
 
 (*---------------------------------------------------------------------------
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Tools/TFL/thry.ML
--- a/src/HOL/Tools/TFL/thry.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Tools/TFL/thry.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Tools/TFL/thry.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 *)
 
 signature THRY =
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/Tools/TFL/utils.ML
--- a/src/HOL/Tools/TFL/utils.ML	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/Tools/TFL/utils.ML	Sun Jan 16 15:53:03 2011 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Tools/TFL/utils.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 
 Basic utilities.
 *)
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/ex/Sudoku.thy
--- a/src/HOL/ex/Sudoku.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/ex/Sudoku.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,5 +1,4 @@
-(*  Title:      Sudoku.thy
-    ID:         $Id$
+(*  Title:      HOL/ex/Sudoku.thy
     Author:     Tjark Weber
     Copyright   2005-2008
 *)
diff -r 9546828c0eb3 -r bbd861837ebc src/HOL/ex/svc_test.thy
--- a/src/HOL/ex/svc_test.thy	Sun Jan 16 15:31:22 2011 +0100
+++ b/src/HOL/ex/svc_test.thy	Sun Jan 16 15:53:03 2011 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 header {* Demonstrating the interface SVC *}
 
 theory svc_test