# HG changeset patch
# User wenzelm
# Date 1268495052 -3600
# Node ID af3ff2ba4c54469d5a99fdff310b90e8f9ca949c
# Parent  c4a698ee83b407ff8af46f18189f8b88fcfc1a27
removed old CVS Ids;
tuned headers;

diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CCL/ex/List.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CCL/ex/List.thy
-    ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CCL/ex/Nat.thy
--- a/src/CCL/ex/Nat.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CCL/ex/Nat.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CCL/ex/Nat.thy
-    ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CCL/ex/ROOT.ML
--- a/src/CCL/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CCL/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CCL/ex/ROOT.ML
-    ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CCL/ex/Stream.thy
--- a/src/CCL/ex/Stream.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CCL/ex/Stream.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CCL/ex/Stream.thy
-    ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/Arith.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/Arith.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/Bool.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/bool
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/CTT.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/CTT.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/Main.thy
--- a/src/CTT/Main.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/Main.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 header {* Main includes everything *}
 
 theory Main
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/ex/Elimination.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,10 +1,9 @@
 (*  Title:      CTT/ex/Elimination.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 Some examples taken from P. Martin-L\"of, Intuitionistic type theory
-        (Bibliopolis, 1984).
+(Bibliopolis, 1984).
 *)
 
 header "Examples with elimination rules"
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/ex/Equality.thy
--- a/src/CTT/ex/Equality.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/ex/Equality.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/ex/Equality.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/ex/ROOT.ML
--- a/src/CTT/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/ex/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/ex/Synthesis.thy
--- a/src/CTT/ex/Synthesis.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/ex/Synthesis.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/ex/Synthesis.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/ex/Typechecking.thy
--- a/src/CTT/ex/Typechecking.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/ex/Typechecking.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/ex/Typechecking.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/CTT/rew.ML
--- a/src/CTT/rew.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/CTT/rew.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      CTT/rew.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Cube/Example.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 header {* Lambda Cube Examples *}
 
 theory Example
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Cube/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Cube/ROOT.ML
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/FOLP.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/FOLP.thy
-    ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/classical.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/classical
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Classical.thy
--- a/src/FOLP/ex/Classical.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Classical.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Classical.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Foundation.thy
--- a/src/FOLP/ex/Foundation.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Foundation.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Foundation.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/If.thy
--- a/src/FOLP/ex/If.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/If.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory If
 imports FOLP
 begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Intro.thy
--- a/src/FOLP/ex/Intro.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Intro.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Intro.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Intuitionistic.thy
--- a/src/FOLP/ex/Intuitionistic.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Intuitionistic.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Intuitionistic.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Nat.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/nat.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Prolog.ML
--- a/src/FOLP/ex/Prolog.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Prolog.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Prolog.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Prolog.thy
--- a/src/FOLP/ex/Prolog.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Prolog.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Prolog.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Propositional_Cla.thy
--- a/src/FOLP/ex/Propositional_Cla.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Propositional_Cla.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Propositional_Cla.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Propositional_Int.thy
--- a/src/FOLP/ex/Propositional_Int.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Propositional_Int.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/Propositional_Int.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Quantifiers_Cla.thy
--- a/src/FOLP/ex/Quantifiers_Cla.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Quantifiers_Cla.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,10 +1,9 @@
 (*  Title:      FOLP/ex/Quantifiers_Cla.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 First-Order Logic: quantifier examples (intuitionistic and classical)
-Needs declarations of the theory "thy" and the tactic "tac"
+Needs declarations of the theory "thy" and the tactic "tac".
 *)
 
 theory Quantifiers_Cla
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/Quantifiers_Int.thy
--- a/src/FOLP/ex/Quantifiers_Int.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/Quantifiers_Int.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,10 +1,9 @@
 (*  Title:      FOLP/ex/Quantifiers_Int.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 First-Order Logic: quantifier examples (intuitionistic and classical)
-Needs declarations of the theory "thy" and the tactic "tac"
+Needs declarations of the theory "thy" and the tactic "tac".
 *)
 
 theory Quantifiers_Int
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/ex/ROOT.ML
--- a/src/FOLP/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/ex/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/hypsubst.ML
--- a/src/FOLP/hypsubst.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/hypsubst.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/hypsubst
-    ID:         $Id$
     Author:     Martin D Coen, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/intprover.ML
--- a/src/FOLP/intprover.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/intprover.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/intprover.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/FOLP/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOLP/simpdata.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/LCF/LCF.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      LCF/LCF.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/LCF/ex/Ex1.thy
--- a/src/LCF/ex/Ex1.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/LCF/ex/Ex1.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 header {*  Section 10.4 *}
 
 theory Ex1
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/LCF/ex/Ex2.thy
--- a/src/LCF/ex/Ex2.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/LCF/ex/Ex2.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 header {* Example 3.8 *}
 
 theory Ex2
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/LCF/ex/Ex3.thy
--- a/src/LCF/ex/Ex3.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/LCF/ex/Ex3.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
 header {* Addition with fixpoint of successor *}
 
 theory Ex3
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/LCF/ex/ROOT.ML
--- a/src/LCF/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/LCF/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      LCF/ex/ROOT.ML
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/abel_cancel.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/abel_cancel.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/assoc_fold.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/assoc_fold.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/cancel_numeral_factor.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/cancel_numerals.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/cancel_numerals.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/combine_numerals.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/combine_numerals.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/extract_common_term.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/extract_common_term.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/Arith/fast_lin_arith.ML
-    ID:         $Id$
     Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
 
 A generic linear arithmetic package.  It provides two tactics
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/hypsubst.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Provers/hypsubst.ML
-    ID:         $Id$
     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     Copyright   1995  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Provers/quantifier1.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      Provers/quantifier1
-    ID:         $Id$
+(*  Title:      Provers/quantifier1.ML
     Author:     Tobias Nipkow
     Copyright   1997  TU Munich
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/ILL_predlog.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory ILL_predlog
 imports ILL
 begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/LK/Hard_Quantifiers.thy
--- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      LK/Hard_Quantifiers.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/LK/Nat.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/LK/Nat.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/LK/Propositional.thy
--- a/src/Sequents/LK/Propositional.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/LK/Propositional.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      LK/Propositional.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/LK/Quantifiers.thy
--- a/src/Sequents/LK/Quantifiers.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/LK/Quantifiers.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      LK/Quantifiers.ML
-    ID:         $Id$
+(*  Title:      LK/Quantifiers.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/LK/ROOT.ML
--- a/src/Sequents/LK/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/LK/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/LK/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/S4.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      Modal/S4.thy
-    ID:         $Id$
+(*  Title:      Sequents/S4.thy
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/T.thy
--- a/src/Sequents/T.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/T.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      Modal/T.thy
-    ID:         $Id$
+(*  Title:      Sequents/T.thy
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/Washing.thy
--- a/src/Sequents/Washing.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/Washing.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
-
-(* $Id$ *)
-
-(* code by Sara Kalvala, based on Paulson's LK
-                           and Moore's tisl.ML *)
+(*  Title:      Sequents/Washing.thy
+    Author:     Sara Kalvala
+*)
 
 theory Washing
 imports ILL
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/Sequents/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/simpdata.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1999  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/AC.thy
--- a/src/ZF/AC.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/AC.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/AC.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
-
 *)
 
 header{*The Axiom of Choice*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Arith.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/Arith.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
 *)
 
 (*"Difference" is subtraction of natural numbers.
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ArithSimp.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/ArithSimp.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
-
 *)
 
 header{*Arithmetic with simplification*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Bool.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/bool.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
 *)
 
 header{*Booleans in Zermelo-Fraenkel Set Theory*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Cardinal_AC.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Cardinal_AC.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Coind/Dynamic.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Coind/Dynamic.thy
-    ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Coind/Language.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Coind/Language.thy
-    ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Coind/Map.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,11 +1,8 @@
 (*  Title:      ZF/Coind/Map.thy
-    ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
-
-Some sample proofs of inclusions for the final coalgebra "U" (by lcp) 
-
+Some sample proofs of inclusions for the final coalgebra "U" (by lcp).
 *)
 
 theory Map imports Main begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Coind/Types.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Coind/Types.thy
-    ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Coind/Values.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Coind/Values.thy
-    ID:         $Id$
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Constructible/ROOT.ML
--- a/src/ZF/Constructible/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Constructible/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,9 +1,8 @@
 (*  Title:      ZF/Constructible/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2002  University of Cambridge
 
-Inner Models, Absoluteness and Consistency Proofs
+Inner Models, Absoluteness and Consistency Proofs.
 *)
 
 use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Epsilon.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
-(*  Title:      ZF/epsilon.thy
-    ID:         $Id$
+(*  Title:      ZF/Epsilon.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
-
 *)
 
 header{*Epsilon Induction and Recursion*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/EquivClass.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/EquivClass.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
-
 *)
 
 header{*Equivalence Relations*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Fixedpt.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      ZF/fixedpt.thy
-    ID:         $Id$
+(*  Title:      ZF/Fixedpt.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/IMP/Com.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/IMP/Com.thy
-    ID:         $Id$
     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/IMP/Denotation.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/IMP/Denotation.thy
-    ID:         $Id$
     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/IMP/Equiv.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/IMP/Equiv.thy
-    ID:         $Id$
     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
 *)
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Acc.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Acc.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Binary_Trees.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Brouwer.thy
--- a/src/ZF/Induct/Brouwer.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Brouwer.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Datatypes.thy
--- a/src/ZF/Induct/Datatypes.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Datatypes.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Datatypes.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/ListN.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/ListN.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Mutil.thy
--- a/src/ZF/Induct/Mutil.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Mutil.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Mutil.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Ntree.thy
--- a/src/ZF/Induct/Ntree.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Ntree.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Ntree.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Primrec.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Primrec.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/PropLog.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/PropLog.thy
-    ID:         $Id$
     Author:     Tobias Nipkow & Lawrence C Paulson
     Copyright   1993  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/ROOT.ML
--- a/src/ZF/Induct/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Rmap.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Rmap.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Term.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Term.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Tree_Forest.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Main.thy
--- a/src/ZF/Main.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Main.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Main 
 imports Main_ZF
 begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Main_ZFC.thy
--- a/src/ZF/Main_ZFC.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Main_ZFC.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(* $Id$ *)
-
-theory Main_ZFC imports Main_ZF InfDatatype begin
+theory Main_ZFC imports Main_ZF InfDatatype
+begin
 
 end
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/OrderArith.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/OrderArith.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
-
 *)
 
 header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Ordinal.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/Ordinal.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
-
 *)
 
 header{*Transitive Sets and Ordinals*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/QPair.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,12 +1,11 @@
-(*  Title:      ZF/qpair.thy
-    ID:         $Id$
+(*  Title:      ZF/QPair.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Many proofs are borrowed from pair.thy and sum.thy
 
 Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
-    is not a limit ordinal? 
+is not a limit ordinal? 
 *)
 
 header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Resid/Confluence.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
-(*  Title:      Confluence.thy
-    ID:         $Id$
+(*  Title:      ZF/Resid/Confluence.thy
     Author:     Ole Rasmussen
     Copyright   1995  University of Cambridge
-    Logic Image: ZF
 *)
 
 theory Confluence imports Reduction begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Resid/Reduction.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
-(*  Title:      Reduction.thy
-    ID:         $Id$
+(*  Title:      ZF/Resid/Reduction.thy
     Author:     Ole Rasmussen
     Copyright   1995  University of Cambridge
-    Logic Image: ZF
 *)
 
 theory Reduction imports Residuals begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Resid/Residuals.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,9 +1,6 @@
-(*  Title:      Residuals.thy
-    ID:         $Id$
+(*  Title:      ZF/Resid/Residuals.thy
     Author:     Ole Rasmussen
     Copyright   1995  University of Cambridge
-    Logic Image: ZF
-
 *)
 
 theory Residuals imports Substitution begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Tools/cartprod.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,11 +1,10 @@
 (*  Title:      ZF/Tools/cartprod.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
-Signatures for inductive definitions
+Signatures for inductive definitions.
 
-Syntactic operations for Cartesian Products
+Syntactic operations for Cartesian Products.
 *)
 
 signature FP =          (** Description of a fixed point operator **)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Tools/ind_cases.ML
-    ID:         $Id$
     Author:     Markus Wenzel, LMU Muenchen
 
 Generic inductive cases facility for (co)inductive definitions.
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Tools/twos_compl.ML
--- a/src/ZF/Tools/twos_compl.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Tools/twos_compl.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Tools/twos_compl.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/Trancl.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
 (*  Title:      ZF/Trancl.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
 *)
 
 header{*Relations: Their General Properties and Transitive Closure*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/UNITY/ROOT.ML
--- a/src/ZF/UNITY/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/UNITY/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/UNITY/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/WF.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/WF.thy
-    ID:         $Id$
     Author:     Tobias Nipkow and Lawrence C Paulson
     Copyright   1994  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/equalities.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,8 +1,6 @@
-(*  Title:      ZF/equalities
-    ID:         $Id$
+(*  Title:      ZF/equalities.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
 *)
 
 header{*Basic Equalities and Inclusions*}
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/BinEx.thy
--- a/src/ZF/ex/BinEx.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/BinEx.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,9 +1,8 @@
-(*  Title:      ZF/ex/BinEx.ML
-    ID:         $Id$
+(*  Title:      ZF/ex/BinEx.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Examples of performing binary arithmetic by simplification
+Examples of performing binary arithmetic by simplification.
 *)
 
 theory BinEx imports Main begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/CoUnit.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      ZF/ex/CoUnit.ML
-    ID:         $Id$
+(*  Title:      ZF/ex/CoUnit.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/Commutation.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,10 +1,8 @@
 (*  Title:      HOL/Lambda/Commutation.thy
-    ID:         $Id$
     Author:     Tobias Nipkow & Sidi Ould Ehmety
     Copyright   1995  TU Muenchen
 
-Commutation theory for proving the Church Rosser theorem
-        ported from Isabelle/HOL  by Sidi Ould Ehmety
+Commutation theory for proving the Church Rosser theorem.
 *)
 
 theory Commutation imports Main begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/NatSum.thy
--- a/src/ZF/ex/NatSum.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/NatSum.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/ex/Natsum.thy
-    ID:         $Id$
     Author:     Tobias Nipkow & Lawrence C Paulson
 
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/ex/ROOT.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/Ramsey.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      ZF/ex/ramsey.thy
-    ID:         $Id$
+(*  Title:      ZF/ex/Ramsey.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
@@ -23,7 +22,6 @@
 fun ram 0 j = 1
   | ram i 0 = 1
   | ram i j = ram (i-1) j + ram i (j-1)
-
 *)
 
 theory Ramsey imports Main begin
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/ex/misc.thy
--- a/src/ZF/ex/misc.thy	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/ex/misc.thy	Sat Mar 13 16:44:12 2010 +0100
@@ -1,5 +1,4 @@
-(*  Title:      ZF/ex/misc.ML
-    ID:         $Id$
+(*  Title:      ZF/ex/misc.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r c4a698ee83b4 -r af3ff2ba4c54 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,9 +1,8 @@
-(*  Title:      ZF/simpdata
-    ID:         $Id$
+(*  Title:      ZF/simpdata.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Rewriting for ZF set theory: specialized extraction of rewrites from theorems
+Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
 *)
 
 (*** New version of mk_rew_rules ***)