removed old CVS Ids;
authorwenzelm
Sat Mar 13 16:44:12 2010 +0100 (2010-03-13)
changeset 35762af3ff2ba4c54
parent 35761 c4a698ee83b4
child 35763 765f8adf10f9
removed old CVS Ids;
tuned headers;
src/CCL/ex/List.thy
src/CCL/ex/Nat.thy
src/CCL/ex/ROOT.ML
src/CCL/ex/Stream.thy
src/CTT/Arith.thy
src/CTT/Bool.thy
src/CTT/CTT.thy
src/CTT/Main.thy
src/CTT/ex/Elimination.thy
src/CTT/ex/Equality.thy
src/CTT/ex/ROOT.ML
src/CTT/ex/Synthesis.thy
src/CTT/ex/Typechecking.thy
src/CTT/rew.ML
src/Cube/Example.thy
src/Cube/ROOT.ML
src/FOLP/FOLP.thy
src/FOLP/classical.ML
src/FOLP/ex/Classical.thy
src/FOLP/ex/Foundation.thy
src/FOLP/ex/If.thy
src/FOLP/ex/Intro.thy
src/FOLP/ex/Intuitionistic.thy
src/FOLP/ex/Nat.thy
src/FOLP/ex/Prolog.ML
src/FOLP/ex/Prolog.thy
src/FOLP/ex/Propositional_Cla.thy
src/FOLP/ex/Propositional_Int.thy
src/FOLP/ex/Quantifiers_Cla.thy
src/FOLP/ex/Quantifiers_Int.thy
src/FOLP/ex/ROOT.ML
src/FOLP/hypsubst.ML
src/FOLP/intprover.ML
src/FOLP/simpdata.ML
src/LCF/LCF.thy
src/LCF/ex/Ex1.thy
src/LCF/ex/Ex2.thy
src/LCF/ex/Ex3.thy
src/LCF/ex/ROOT.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.ML
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/Arith/extract_common_term.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Provers/quantifier1.ML
src/Sequents/ILL_predlog.thy
src/Sequents/LK/Hard_Quantifiers.thy
src/Sequents/LK/Nat.thy
src/Sequents/LK/Propositional.thy
src/Sequents/LK/Quantifiers.thy
src/Sequents/LK/ROOT.ML
src/Sequents/ROOT.ML
src/Sequents/S4.thy
src/Sequents/T.thy
src/Sequents/Washing.thy
src/Sequents/simpdata.ML
src/ZF/AC.thy
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/Bool.thy
src/ZF/Cardinal_AC.thy
src/ZF/Coind/Dynamic.thy
src/ZF/Coind/Language.thy
src/ZF/Coind/Map.thy
src/ZF/Coind/Types.thy
src/ZF/Coind/Values.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Epsilon.thy
src/ZF/EquivClass.thy
src/ZF/Fixedpt.thy
src/ZF/IMP/Com.thy
src/ZF/IMP/Denotation.thy
src/ZF/IMP/Equiv.thy
src/ZF/Induct/Acc.thy
src/ZF/Induct/Binary_Trees.thy
src/ZF/Induct/Brouwer.thy
src/ZF/Induct/Datatypes.thy
src/ZF/Induct/ListN.thy
src/ZF/Induct/Mutil.thy
src/ZF/Induct/Ntree.thy
src/ZF/Induct/Primrec.thy
src/ZF/Induct/PropLog.thy
src/ZF/Induct/ROOT.ML
src/ZF/Induct/Rmap.thy
src/ZF/Induct/Term.thy
src/ZF/Induct/Tree_Forest.thy
src/ZF/Main.thy
src/ZF/Main_ZFC.thy
src/ZF/OrderArith.thy
src/ZF/Ordinal.thy
src/ZF/QPair.thy
src/ZF/ROOT.ML
src/ZF/Resid/Confluence.thy
src/ZF/Resid/Reduction.thy
src/ZF/Resid/Residuals.thy
src/ZF/Tools/cartprod.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/twos_compl.ML
src/ZF/Trancl.thy
src/ZF/UNITY/ROOT.ML
src/ZF/WF.thy
src/ZF/equalities.thy
src/ZF/ex/BinEx.thy
src/ZF/ex/CoUnit.thy
src/ZF/ex/Commutation.thy
src/ZF/ex/NatSum.thy
src/ZF/ex/ROOT.ML
src/ZF/ex/Ramsey.thy
src/ZF/ex/misc.thy
src/ZF/simpdata.ML
     1.1 --- a/src/CCL/ex/List.thy	Sat Mar 13 16:37:15 2010 +0100
     1.2 +++ b/src/CCL/ex/List.thy	Sat Mar 13 16:44:12 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      CCL/ex/List.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Martin Coen, Cambridge University Computer Laboratory
     1.7      Copyright   1993  University of Cambridge
     1.8  *)
     2.1 --- a/src/CCL/ex/Nat.thy	Sat Mar 13 16:37:15 2010 +0100
     2.2 +++ b/src/CCL/ex/Nat.thy	Sat Mar 13 16:44:12 2010 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      CCL/ex/Nat.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Martin Coen, Cambridge University Computer Laboratory
     2.7      Copyright   1993  University of Cambridge
     2.8  *)
     3.1 --- a/src/CCL/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
     3.2 +++ b/src/CCL/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      CCL/ex/ROOT.ML
     3.5 -    ID:         $Id$
     3.6      Author:     Martin Coen, Cambridge University Computer Laboratory
     3.7      Copyright   1993  University of Cambridge
     3.8  
     4.1 --- a/src/CCL/ex/Stream.thy	Sat Mar 13 16:37:15 2010 +0100
     4.2 +++ b/src/CCL/ex/Stream.thy	Sat Mar 13 16:44:12 2010 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      CCL/ex/Stream.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Martin Coen, Cambridge University Computer Laboratory
     4.7      Copyright   1993  University of Cambridge
     4.8  *)
     5.1 --- a/src/CTT/Arith.thy	Sat Mar 13 16:37:15 2010 +0100
     5.2 +++ b/src/CTT/Arith.thy	Sat Mar 13 16:44:12 2010 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      CTT/Arith.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7      Copyright   1991  University of Cambridge
     5.8  *)
     6.1 --- a/src/CTT/Bool.thy	Sat Mar 13 16:37:15 2010 +0100
     6.2 +++ b/src/CTT/Bool.thy	Sat Mar 13 16:44:12 2010 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      CTT/bool
     6.5 -    ID:         $Id$
     6.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7      Copyright   1991  University of Cambridge
     6.8  *)
     7.1 --- a/src/CTT/CTT.thy	Sat Mar 13 16:37:15 2010 +0100
     7.2 +++ b/src/CTT/CTT.thy	Sat Mar 13 16:44:12 2010 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      CTT/CTT.thy
     7.5 -    ID:         $Id$
     7.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7      Copyright   1993  University of Cambridge
     7.8  *)
     8.1 --- a/src/CTT/Main.thy	Sat Mar 13 16:37:15 2010 +0100
     8.2 +++ b/src/CTT/Main.thy	Sat Mar 13 16:44:12 2010 +0100
     8.3 @@ -1,6 +1,3 @@
     8.4 -
     8.5 -(* $Id$ *)
     8.6 -
     8.7  header {* Main includes everything *}
     8.8  
     8.9  theory Main
     9.1 --- a/src/CTT/ex/Elimination.thy	Sat Mar 13 16:37:15 2010 +0100
     9.2 +++ b/src/CTT/ex/Elimination.thy	Sat Mar 13 16:44:12 2010 +0100
     9.3 @@ -1,10 +1,9 @@
     9.4  (*  Title:      CTT/ex/Elimination.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7      Copyright   1991  University of Cambridge
     9.8  
     9.9  Some examples taken from P. Martin-L\"of, Intuitionistic type theory
    9.10 -        (Bibliopolis, 1984).
    9.11 +(Bibliopolis, 1984).
    9.12  *)
    9.13  
    9.14  header "Examples with elimination rules"
    10.1 --- a/src/CTT/ex/Equality.thy	Sat Mar 13 16:37:15 2010 +0100
    10.2 +++ b/src/CTT/ex/Equality.thy	Sat Mar 13 16:44:12 2010 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      CTT/ex/Equality.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7      Copyright   1991  University of Cambridge
    10.8  *)
    11.1 --- a/src/CTT/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    11.2 +++ b/src/CTT/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      CTT/ex/ROOT.ML
    11.5 -    ID:         $Id$
    11.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7      Copyright   1991  University of Cambridge
    11.8  
    12.1 --- a/src/CTT/ex/Synthesis.thy	Sat Mar 13 16:37:15 2010 +0100
    12.2 +++ b/src/CTT/ex/Synthesis.thy	Sat Mar 13 16:44:12 2010 +0100
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      CTT/ex/Synthesis.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7      Copyright   1991  University of Cambridge
    12.8  *)
    13.1 --- a/src/CTT/ex/Typechecking.thy	Sat Mar 13 16:37:15 2010 +0100
    13.2 +++ b/src/CTT/ex/Typechecking.thy	Sat Mar 13 16:44:12 2010 +0100
    13.3 @@ -1,5 +1,4 @@
    13.4  (*  Title:      CTT/ex/Typechecking.thy
    13.5 -    ID:         $Id$
    13.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7      Copyright   1991  University of Cambridge
    13.8  *)
    14.1 --- a/src/CTT/rew.ML	Sat Mar 13 16:37:15 2010 +0100
    14.2 +++ b/src/CTT/rew.ML	Sat Mar 13 16:44:12 2010 +0100
    14.3 @@ -1,5 +1,4 @@
    14.4  (*  Title:      CTT/rew.ML
    14.5 -    ID:         $Id$
    14.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7      Copyright   1991  University of Cambridge
    14.8  
    15.1 --- a/src/Cube/Example.thy	Sat Mar 13 16:37:15 2010 +0100
    15.2 +++ b/src/Cube/Example.thy	Sat Mar 13 16:44:12 2010 +0100
    15.3 @@ -1,6 +1,3 @@
    15.4 -
    15.5 -(* $Id$ *)
    15.6 -
    15.7  header {* Lambda Cube Examples *}
    15.8  
    15.9  theory Example
    16.1 --- a/src/Cube/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    16.2 +++ b/src/Cube/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    16.3 @@ -1,5 +1,4 @@
    16.4  (*  Title:      Cube/ROOT.ML
    16.5 -    ID:         $Id$
    16.6      Author:     Tobias Nipkow
    16.7      Copyright   1992  University of Cambridge
    16.8  
    17.1 --- a/src/FOLP/FOLP.thy	Sat Mar 13 16:37:15 2010 +0100
    17.2 +++ b/src/FOLP/FOLP.thy	Sat Mar 13 16:44:12 2010 +0100
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      FOLP/FOLP.thy
    17.5 -    ID:         $Id$
    17.6      Author:     Martin D Coen, Cambridge University Computer Laboratory
    17.7      Copyright   1992  University of Cambridge
    17.8  *)
    18.1 --- a/src/FOLP/classical.ML	Sat Mar 13 16:37:15 2010 +0100
    18.2 +++ b/src/FOLP/classical.ML	Sat Mar 13 16:44:12 2010 +0100
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      FOLP/classical
    18.5 -    ID:         $Id$
    18.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7      Copyright   1992  University of Cambridge
    18.8  
    19.1 --- a/src/FOLP/ex/Classical.thy	Sat Mar 13 16:37:15 2010 +0100
    19.2 +++ b/src/FOLP/ex/Classical.thy	Sat Mar 13 16:44:12 2010 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      FOLP/ex/Classical.thy
    19.5 -    ID:         $Id$
    19.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7      Copyright   1993  University of Cambridge
    19.8  
    20.1 --- a/src/FOLP/ex/Foundation.thy	Sat Mar 13 16:37:15 2010 +0100
    20.2 +++ b/src/FOLP/ex/Foundation.thy	Sat Mar 13 16:44:12 2010 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      FOLP/ex/Foundation.ML
    20.5 -    ID:         $Id$
    20.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7      Copyright   1991  University of Cambridge
    20.8  *)
    21.1 --- a/src/FOLP/ex/If.thy	Sat Mar 13 16:37:15 2010 +0100
    21.2 +++ b/src/FOLP/ex/If.thy	Sat Mar 13 16:44:12 2010 +0100
    21.3 @@ -1,5 +1,3 @@
    21.4 -(* $Id$ *)
    21.5 -
    21.6  theory If
    21.7  imports FOLP
    21.8  begin
    22.1 --- a/src/FOLP/ex/Intro.thy	Sat Mar 13 16:37:15 2010 +0100
    22.2 +++ b/src/FOLP/ex/Intro.thy	Sat Mar 13 16:44:12 2010 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      FOLP/ex/Intro.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7      Copyright   1992  University of Cambridge
    22.8  
    23.1 --- a/src/FOLP/ex/Intuitionistic.thy	Sat Mar 13 16:37:15 2010 +0100
    23.2 +++ b/src/FOLP/ex/Intuitionistic.thy	Sat Mar 13 16:44:12 2010 +0100
    23.3 @@ -1,5 +1,4 @@
    23.4  (*  Title:      FOLP/ex/Intuitionistic.thy
    23.5 -    ID:         $Id$
    23.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7      Copyright   1991  University of Cambridge
    23.8  
    24.1 --- a/src/FOLP/ex/Nat.thy	Sat Mar 13 16:37:15 2010 +0100
    24.2 +++ b/src/FOLP/ex/Nat.thy	Sat Mar 13 16:44:12 2010 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      FOLP/ex/nat.thy
    24.5 -    ID:         $Id$
    24.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7      Copyright   1992  University of Cambridge
    24.8  *)
    25.1 --- a/src/FOLP/ex/Prolog.ML	Sat Mar 13 16:37:15 2010 +0100
    25.2 +++ b/src/FOLP/ex/Prolog.ML	Sat Mar 13 16:44:12 2010 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      FOLP/ex/Prolog.ML
    25.5 -    ID:         $Id$
    25.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7      Copyright   1992  University of Cambridge
    25.8  
    26.1 --- a/src/FOLP/ex/Prolog.thy	Sat Mar 13 16:37:15 2010 +0100
    26.2 +++ b/src/FOLP/ex/Prolog.thy	Sat Mar 13 16:44:12 2010 +0100
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:      FOLP/ex/Prolog.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.7      Copyright   1992  University of Cambridge
    26.8  
    27.1 --- a/src/FOLP/ex/Propositional_Cla.thy	Sat Mar 13 16:37:15 2010 +0100
    27.2 +++ b/src/FOLP/ex/Propositional_Cla.thy	Sat Mar 13 16:44:12 2010 +0100
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      FOLP/ex/Propositional_Cla.thy
    27.5 -    ID:         $Id$
    27.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    27.7      Copyright   1991  University of Cambridge
    27.8  *)
    28.1 --- a/src/FOLP/ex/Propositional_Int.thy	Sat Mar 13 16:37:15 2010 +0100
    28.2 +++ b/src/FOLP/ex/Propositional_Int.thy	Sat Mar 13 16:44:12 2010 +0100
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      FOLP/ex/Propositional_Int.thy
    28.5 -    ID:         $Id$
    28.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.7      Copyright   1991  University of Cambridge
    28.8  *)
    29.1 --- a/src/FOLP/ex/Quantifiers_Cla.thy	Sat Mar 13 16:37:15 2010 +0100
    29.2 +++ b/src/FOLP/ex/Quantifiers_Cla.thy	Sat Mar 13 16:44:12 2010 +0100
    29.3 @@ -1,10 +1,9 @@
    29.4  (*  Title:      FOLP/ex/Quantifiers_Cla.thy
    29.5 -    ID:         $Id$
    29.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    29.7      Copyright   1991  University of Cambridge
    29.8  
    29.9  First-Order Logic: quantifier examples (intuitionistic and classical)
   29.10 -Needs declarations of the theory "thy" and the tactic "tac"
   29.11 +Needs declarations of the theory "thy" and the tactic "tac".
   29.12  *)
   29.13  
   29.14  theory Quantifiers_Cla
    30.1 --- a/src/FOLP/ex/Quantifiers_Int.thy	Sat Mar 13 16:37:15 2010 +0100
    30.2 +++ b/src/FOLP/ex/Quantifiers_Int.thy	Sat Mar 13 16:44:12 2010 +0100
    30.3 @@ -1,10 +1,9 @@
    30.4  (*  Title:      FOLP/ex/Quantifiers_Int.thy
    30.5 -    ID:         $Id$
    30.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    30.7      Copyright   1991  University of Cambridge
    30.8  
    30.9  First-Order Logic: quantifier examples (intuitionistic and classical)
   30.10 -Needs declarations of the theory "thy" and the tactic "tac"
   30.11 +Needs declarations of the theory "thy" and the tactic "tac".
   30.12  *)
   30.13  
   30.14  theory Quantifiers_Int
    31.1 --- a/src/FOLP/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    31.2 +++ b/src/FOLP/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    31.3 @@ -1,5 +1,4 @@
    31.4  (*  Title:      FOLP/ex/ROOT.ML
    31.5 -    ID:         $Id$
    31.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    31.7      Copyright   1992  University of Cambridge
    31.8  
    32.1 --- a/src/FOLP/hypsubst.ML	Sat Mar 13 16:37:15 2010 +0100
    32.2 +++ b/src/FOLP/hypsubst.ML	Sat Mar 13 16:44:12 2010 +0100
    32.3 @@ -1,5 +1,4 @@
    32.4  (*  Title:      FOLP/hypsubst
    32.5 -    ID:         $Id$
    32.6      Author:     Martin D Coen, Cambridge University Computer Laboratory
    32.7      Copyright   1995  University of Cambridge
    32.8  
    33.1 --- a/src/FOLP/intprover.ML	Sat Mar 13 16:37:15 2010 +0100
    33.2 +++ b/src/FOLP/intprover.ML	Sat Mar 13 16:44:12 2010 +0100
    33.3 @@ -1,5 +1,4 @@
    33.4  (*  Title:      FOLP/intprover.ML
    33.5 -    ID:         $Id$
    33.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    33.7      Copyright   1992  University of Cambridge
    33.8  
    34.1 --- a/src/FOLP/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
    34.2 +++ b/src/FOLP/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
    34.3 @@ -1,5 +1,4 @@
    34.4  (*  Title:      FOLP/simpdata.ML
    34.5 -    ID:         $Id$
    34.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    34.7      Copyright   1991  University of Cambridge
    34.8  
    35.1 --- a/src/LCF/LCF.thy	Sat Mar 13 16:37:15 2010 +0100
    35.2 +++ b/src/LCF/LCF.thy	Sat Mar 13 16:44:12 2010 +0100
    35.3 @@ -1,5 +1,4 @@
    35.4  (*  Title:      LCF/LCF.thy
    35.5 -    ID:         $Id$
    35.6      Author:     Tobias Nipkow
    35.7      Copyright   1992  University of Cambridge
    35.8  *)
    36.1 --- a/src/LCF/ex/Ex1.thy	Sat Mar 13 16:37:15 2010 +0100
    36.2 +++ b/src/LCF/ex/Ex1.thy	Sat Mar 13 16:44:12 2010 +0100
    36.3 @@ -1,6 +1,3 @@
    36.4 -
    36.5 -(* $Id$ *)
    36.6 -
    36.7  header {*  Section 10.4 *}
    36.8  
    36.9  theory Ex1
    37.1 --- a/src/LCF/ex/Ex2.thy	Sat Mar 13 16:37:15 2010 +0100
    37.2 +++ b/src/LCF/ex/Ex2.thy	Sat Mar 13 16:44:12 2010 +0100
    37.3 @@ -1,6 +1,3 @@
    37.4 -
    37.5 -(* $Id$ *)
    37.6 -
    37.7  header {* Example 3.8 *}
    37.8  
    37.9  theory Ex2
    38.1 --- a/src/LCF/ex/Ex3.thy	Sat Mar 13 16:37:15 2010 +0100
    38.2 +++ b/src/LCF/ex/Ex3.thy	Sat Mar 13 16:44:12 2010 +0100
    38.3 @@ -1,6 +1,3 @@
    38.4 -
    38.5 -(* $Id$ *)
    38.6 -
    38.7  header {* Addition with fixpoint of successor *}
    38.8  
    38.9  theory Ex3
    39.1 --- a/src/LCF/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    39.2 +++ b/src/LCF/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    39.3 @@ -1,5 +1,4 @@
    39.4  (*  Title:      LCF/ex/ROOT.ML
    39.5 -    ID:         $Id$
    39.6      Author:     Tobias Nipkow
    39.7      Copyright   1991  University of Cambridge
    39.8  
    40.1 --- a/src/Provers/Arith/abel_cancel.ML	Sat Mar 13 16:37:15 2010 +0100
    40.2 +++ b/src/Provers/Arith/abel_cancel.ML	Sat Mar 13 16:44:12 2010 +0100
    40.3 @@ -1,5 +1,4 @@
    40.4  (*  Title:      Provers/Arith/abel_cancel.ML
    40.5 -    ID:         $Id$
    40.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    40.7      Copyright   1998  University of Cambridge
    40.8  
    41.1 --- a/src/Provers/Arith/assoc_fold.ML	Sat Mar 13 16:37:15 2010 +0100
    41.2 +++ b/src/Provers/Arith/assoc_fold.ML	Sat Mar 13 16:44:12 2010 +0100
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title:      Provers/Arith/assoc_fold.ML
    41.5 -    ID:         $Id$
    41.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    41.7      Copyright   1999  University of Cambridge
    41.8  
    42.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Sat Mar 13 16:37:15 2010 +0100
    42.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Sat Mar 13 16:44:12 2010 +0100
    42.3 @@ -1,5 +1,4 @@
    42.4  (*  Title:      Provers/Arith/cancel_numeral_factor.ML
    42.5 -    ID:         $Id$
    42.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    42.7      Copyright   2000  University of Cambridge
    42.8  
    43.1 --- a/src/Provers/Arith/cancel_numerals.ML	Sat Mar 13 16:37:15 2010 +0100
    43.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Sat Mar 13 16:44:12 2010 +0100
    43.3 @@ -1,5 +1,4 @@
    43.4  (*  Title:      Provers/Arith/cancel_numerals.ML
    43.5 -    ID:         $Id$
    43.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.7      Copyright   2000  University of Cambridge
    43.8  
    44.1 --- a/src/Provers/Arith/combine_numerals.ML	Sat Mar 13 16:37:15 2010 +0100
    44.2 +++ b/src/Provers/Arith/combine_numerals.ML	Sat Mar 13 16:44:12 2010 +0100
    44.3 @@ -1,5 +1,4 @@
    44.4  (*  Title:      Provers/Arith/combine_numerals.ML
    44.5 -    ID:         $Id$
    44.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    44.7      Copyright   2000  University of Cambridge
    44.8  
    45.1 --- a/src/Provers/Arith/extract_common_term.ML	Sat Mar 13 16:37:15 2010 +0100
    45.2 +++ b/src/Provers/Arith/extract_common_term.ML	Sat Mar 13 16:44:12 2010 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      Provers/Arith/extract_common_term.ML
    45.5 -    ID:         $Id$
    45.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    45.7      Copyright   2000  University of Cambridge
    45.8  
    46.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat Mar 13 16:37:15 2010 +0100
    46.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Mar 13 16:44:12 2010 +0100
    46.3 @@ -1,5 +1,4 @@
    46.4  (*  Title:      Provers/Arith/fast_lin_arith.ML
    46.5 -    ID:         $Id$
    46.6      Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
    46.7  
    46.8  A generic linear arithmetic package.  It provides two tactics
    47.1 --- a/src/Provers/hypsubst.ML	Sat Mar 13 16:37:15 2010 +0100
    47.2 +++ b/src/Provers/hypsubst.ML	Sat Mar 13 16:44:12 2010 +0100
    47.3 @@ -1,5 +1,4 @@
    47.4  (*  Title:      Provers/hypsubst.ML
    47.5 -    ID:         $Id$
    47.6      Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
    47.7      Copyright   1995  University of Cambridge
    47.8  
    48.1 --- a/src/Provers/quantifier1.ML	Sat Mar 13 16:37:15 2010 +0100
    48.2 +++ b/src/Provers/quantifier1.ML	Sat Mar 13 16:44:12 2010 +0100
    48.3 @@ -1,5 +1,4 @@
    48.4 -(*  Title:      Provers/quantifier1
    48.5 -    ID:         $Id$
    48.6 +(*  Title:      Provers/quantifier1.ML
    48.7      Author:     Tobias Nipkow
    48.8      Copyright   1997  TU Munich
    48.9  
    49.1 --- a/src/Sequents/ILL_predlog.thy	Sat Mar 13 16:37:15 2010 +0100
    49.2 +++ b/src/Sequents/ILL_predlog.thy	Sat Mar 13 16:44:12 2010 +0100
    49.3 @@ -1,5 +1,3 @@
    49.4 -(* $Id$ *)
    49.5 -
    49.6  theory ILL_predlog
    49.7  imports ILL
    49.8  begin
    50.1 --- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Mar 13 16:37:15 2010 +0100
    50.2 +++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Mar 13 16:44:12 2010 +0100
    50.3 @@ -1,5 +1,4 @@
    50.4  (*  Title:      LK/Hard_Quantifiers.thy
    50.5 -    ID:         $Id$
    50.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    50.7      Copyright   1992  University of Cambridge
    50.8  
    51.1 --- a/src/Sequents/LK/Nat.thy	Sat Mar 13 16:37:15 2010 +0100
    51.2 +++ b/src/Sequents/LK/Nat.thy	Sat Mar 13 16:44:12 2010 +0100
    51.3 @@ -1,5 +1,4 @@
    51.4  (*  Title:      Sequents/LK/Nat.thy
    51.5 -    ID:         $Id$
    51.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    51.7      Copyright   1999  University of Cambridge
    51.8  *)
    52.1 --- a/src/Sequents/LK/Propositional.thy	Sat Mar 13 16:37:15 2010 +0100
    52.2 +++ b/src/Sequents/LK/Propositional.thy	Sat Mar 13 16:44:12 2010 +0100
    52.3 @@ -1,5 +1,4 @@
    52.4  (*  Title:      LK/Propositional.thy
    52.5 -    ID:         $Id$
    52.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    52.7      Copyright   1992  University of Cambridge
    52.8  *)
    53.1 --- a/src/Sequents/LK/Quantifiers.thy	Sat Mar 13 16:37:15 2010 +0100
    53.2 +++ b/src/Sequents/LK/Quantifiers.thy	Sat Mar 13 16:44:12 2010 +0100
    53.3 @@ -1,5 +1,4 @@
    53.4 -(*  Title:      LK/Quantifiers.ML
    53.5 -    ID:         $Id$
    53.6 +(*  Title:      LK/Quantifiers.thy
    53.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    53.8      Copyright   1992  University of Cambridge
    53.9  
    54.1 --- a/src/Sequents/LK/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    54.2 +++ b/src/Sequents/LK/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    54.3 @@ -1,5 +1,4 @@
    54.4  (*  Title:      Sequents/LK/ROOT.ML
    54.5 -    ID:         $Id$
    54.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54.7      Copyright   1992  University of Cambridge
    54.8  
    55.1 --- a/src/Sequents/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    55.2 +++ b/src/Sequents/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    55.3 @@ -1,5 +1,4 @@
    55.4  (*  Title:      Sequents/ROOT.ML
    55.5 -    ID:         $Id$
    55.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    55.7      Copyright   1991  University of Cambridge
    55.8  
    56.1 --- a/src/Sequents/S4.thy	Sat Mar 13 16:37:15 2010 +0100
    56.2 +++ b/src/Sequents/S4.thy	Sat Mar 13 16:44:12 2010 +0100
    56.3 @@ -1,5 +1,4 @@
    56.4 -(*  Title:      Modal/S4.thy
    56.5 -    ID:         $Id$
    56.6 +(*  Title:      Sequents/S4.thy
    56.7      Author:     Martin Coen
    56.8      Copyright   1991  University of Cambridge
    56.9  *)
    57.1 --- a/src/Sequents/T.thy	Sat Mar 13 16:37:15 2010 +0100
    57.2 +++ b/src/Sequents/T.thy	Sat Mar 13 16:44:12 2010 +0100
    57.3 @@ -1,5 +1,4 @@
    57.4 -(*  Title:      Modal/T.thy
    57.5 -    ID:         $Id$
    57.6 +(*  Title:      Sequents/T.thy
    57.7      Author:     Martin Coen
    57.8      Copyright   1991  University of Cambridge
    57.9  *)
    58.1 --- a/src/Sequents/Washing.thy	Sat Mar 13 16:37:15 2010 +0100
    58.2 +++ b/src/Sequents/Washing.thy	Sat Mar 13 16:44:12 2010 +0100
    58.3 @@ -1,8 +1,6 @@
    58.4 -
    58.5 -(* $Id$ *)
    58.6 -
    58.7 -(* code by Sara Kalvala, based on Paulson's LK
    58.8 -                           and Moore's tisl.ML *)
    58.9 +(*  Title:      Sequents/Washing.thy
   58.10 +    Author:     Sara Kalvala
   58.11 +*)
   58.12  
   58.13  theory Washing
   58.14  imports ILL
    59.1 --- a/src/Sequents/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
    59.2 +++ b/src/Sequents/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
    59.3 @@ -1,5 +1,4 @@
    59.4  (*  Title:      Sequents/simpdata.ML
    59.5 -    ID:         $Id$
    59.6      Author:     Lawrence C Paulson
    59.7      Copyright   1999  University of Cambridge
    59.8  
    60.1 --- a/src/ZF/AC.thy	Sat Mar 13 16:37:15 2010 +0100
    60.2 +++ b/src/ZF/AC.thy	Sat Mar 13 16:44:12 2010 +0100
    60.3 @@ -1,8 +1,6 @@
    60.4  (*  Title:      ZF/AC.thy
    60.5 -    ID:         $Id$
    60.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    60.7      Copyright   1994  University of Cambridge
    60.8 -
    60.9  *)
   60.10  
   60.11  header{*The Axiom of Choice*}
    61.1 --- a/src/ZF/Arith.thy	Sat Mar 13 16:37:15 2010 +0100
    61.2 +++ b/src/ZF/Arith.thy	Sat Mar 13 16:44:12 2010 +0100
    61.3 @@ -1,8 +1,6 @@
    61.4  (*  Title:      ZF/Arith.thy
    61.5 -    ID:         $Id$
    61.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    61.7      Copyright   1992  University of Cambridge
    61.8 -
    61.9  *)
   61.10  
   61.11  (*"Difference" is subtraction of natural numbers.
    62.1 --- a/src/ZF/ArithSimp.thy	Sat Mar 13 16:37:15 2010 +0100
    62.2 +++ b/src/ZF/ArithSimp.thy	Sat Mar 13 16:44:12 2010 +0100
    62.3 @@ -1,8 +1,6 @@
    62.4  (*  Title:      ZF/ArithSimp.ML
    62.5 -    ID:         $Id$
    62.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    62.7      Copyright   2000  University of Cambridge
    62.8 -
    62.9  *)
   62.10  
   62.11  header{*Arithmetic with simplification*}
    63.1 --- a/src/ZF/Bool.thy	Sat Mar 13 16:37:15 2010 +0100
    63.2 +++ b/src/ZF/Bool.thy	Sat Mar 13 16:44:12 2010 +0100
    63.3 @@ -1,8 +1,6 @@
    63.4  (*  Title:      ZF/bool.thy
    63.5 -    ID:         $Id$
    63.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    63.7      Copyright   1992  University of Cambridge
    63.8 -
    63.9  *)
   63.10  
   63.11  header{*Booleans in Zermelo-Fraenkel Set Theory*}
    64.1 --- a/src/ZF/Cardinal_AC.thy	Sat Mar 13 16:37:15 2010 +0100
    64.2 +++ b/src/ZF/Cardinal_AC.thy	Sat Mar 13 16:44:12 2010 +0100
    64.3 @@ -1,5 +1,4 @@
    64.4  (*  Title:      ZF/Cardinal_AC.thy
    64.5 -    ID:         $Id$
    64.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    64.7      Copyright   1994  University of Cambridge
    64.8  
    65.1 --- a/src/ZF/Coind/Dynamic.thy	Sat Mar 13 16:37:15 2010 +0100
    65.2 +++ b/src/ZF/Coind/Dynamic.thy	Sat Mar 13 16:44:12 2010 +0100
    65.3 @@ -1,5 +1,4 @@
    65.4  (*  Title:      ZF/Coind/Dynamic.thy
    65.5 -    ID:         $Id$
    65.6      Author:     Jacob Frost, Cambridge University Computer Laboratory
    65.7      Copyright   1995  University of Cambridge
    65.8  *)
    66.1 --- a/src/ZF/Coind/Language.thy	Sat Mar 13 16:37:15 2010 +0100
    66.2 +++ b/src/ZF/Coind/Language.thy	Sat Mar 13 16:44:12 2010 +0100
    66.3 @@ -1,5 +1,4 @@
    66.4  (*  Title:      ZF/Coind/Language.thy
    66.5 -    ID:         $Id$
    66.6      Author:     Jacob Frost, Cambridge University Computer Laboratory
    66.7      Copyright   1995  University of Cambridge
    66.8  *)
    67.1 --- a/src/ZF/Coind/Map.thy	Sat Mar 13 16:37:15 2010 +0100
    67.2 +++ b/src/ZF/Coind/Map.thy	Sat Mar 13 16:44:12 2010 +0100
    67.3 @@ -1,11 +1,8 @@
    67.4  (*  Title:      ZF/Coind/Map.thy
    67.5 -    ID:         $Id$
    67.6      Author:     Jacob Frost, Cambridge University Computer Laboratory
    67.7      Copyright   1995  University of Cambridge
    67.8  
    67.9 -
   67.10 -Some sample proofs of inclusions for the final coalgebra "U" (by lcp) 
   67.11 -
   67.12 +Some sample proofs of inclusions for the final coalgebra "U" (by lcp).
   67.13  *)
   67.14  
   67.15  theory Map imports Main begin
    68.1 --- a/src/ZF/Coind/Types.thy	Sat Mar 13 16:37:15 2010 +0100
    68.2 +++ b/src/ZF/Coind/Types.thy	Sat Mar 13 16:44:12 2010 +0100
    68.3 @@ -1,5 +1,4 @@
    68.4  (*  Title:      ZF/Coind/Types.thy
    68.5 -    ID:         $Id$
    68.6      Author:     Jacob Frost, Cambridge University Computer Laboratory
    68.7      Copyright   1995  University of Cambridge
    68.8  *)
    69.1 --- a/src/ZF/Coind/Values.thy	Sat Mar 13 16:37:15 2010 +0100
    69.2 +++ b/src/ZF/Coind/Values.thy	Sat Mar 13 16:44:12 2010 +0100
    69.3 @@ -1,5 +1,4 @@
    69.4  (*  Title:      ZF/Coind/Values.thy
    69.5 -    ID:         $Id$
    69.6      Author:     Jacob Frost, Cambridge University Computer Laboratory
    69.7      Copyright   1995  University of Cambridge
    69.8  *)
    70.1 --- a/src/ZF/Constructible/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    70.2 +++ b/src/ZF/Constructible/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    70.3 @@ -1,9 +1,8 @@
    70.4  (*  Title:      ZF/Constructible/ROOT.ML
    70.5 -    ID:         $Id$
    70.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    70.7      Copyright   2002  University of Cambridge
    70.8  
    70.9 -Inner Models, Absoluteness and Consistency Proofs
   70.10 +Inner Models, Absoluteness and Consistency Proofs.
   70.11  *)
   70.12  
   70.13  use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];
    71.1 --- a/src/ZF/Epsilon.thy	Sat Mar 13 16:37:15 2010 +0100
    71.2 +++ b/src/ZF/Epsilon.thy	Sat Mar 13 16:44:12 2010 +0100
    71.3 @@ -1,8 +1,6 @@
    71.4 -(*  Title:      ZF/epsilon.thy
    71.5 -    ID:         $Id$
    71.6 +(*  Title:      ZF/Epsilon.thy
    71.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    71.8      Copyright   1993  University of Cambridge
    71.9 -
   71.10  *)
   71.11  
   71.12  header{*Epsilon Induction and Recursion*}
    72.1 --- a/src/ZF/EquivClass.thy	Sat Mar 13 16:37:15 2010 +0100
    72.2 +++ b/src/ZF/EquivClass.thy	Sat Mar 13 16:44:12 2010 +0100
    72.3 @@ -1,8 +1,6 @@
    72.4  (*  Title:      ZF/EquivClass.thy
    72.5 -    ID:         $Id$
    72.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    72.7      Copyright   1994  University of Cambridge
    72.8 -
    72.9  *)
   72.10  
   72.11  header{*Equivalence Relations*}
    73.1 --- a/src/ZF/Fixedpt.thy	Sat Mar 13 16:37:15 2010 +0100
    73.2 +++ b/src/ZF/Fixedpt.thy	Sat Mar 13 16:44:12 2010 +0100
    73.3 @@ -1,5 +1,4 @@
    73.4 -(*  Title:      ZF/fixedpt.thy
    73.5 -    ID:         $Id$
    73.6 +(*  Title:      ZF/Fixedpt.thy
    73.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    73.8      Copyright   1992  University of Cambridge
    73.9  *)
    74.1 --- a/src/ZF/IMP/Com.thy	Sat Mar 13 16:37:15 2010 +0100
    74.2 +++ b/src/ZF/IMP/Com.thy	Sat Mar 13 16:44:12 2010 +0100
    74.3 @@ -1,5 +1,4 @@
    74.4  (*  Title:      ZF/IMP/Com.thy
    74.5 -    ID:         $Id$
    74.6      Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    74.7  *)
    74.8  
    75.1 --- a/src/ZF/IMP/Denotation.thy	Sat Mar 13 16:37:15 2010 +0100
    75.2 +++ b/src/ZF/IMP/Denotation.thy	Sat Mar 13 16:44:12 2010 +0100
    75.3 @@ -1,5 +1,4 @@
    75.4  (*  Title:      ZF/IMP/Denotation.thy
    75.5 -    ID:         $Id$
    75.6      Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    75.7  *)
    75.8  
    76.1 --- a/src/ZF/IMP/Equiv.thy	Sat Mar 13 16:37:15 2010 +0100
    76.2 +++ b/src/ZF/IMP/Equiv.thy	Sat Mar 13 16:44:12 2010 +0100
    76.3 @@ -1,5 +1,4 @@
    76.4  (*  Title:      ZF/IMP/Equiv.thy
    76.5 -    ID:         $Id$
    76.6      Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    76.7  *)
    76.8  
    77.1 --- a/src/ZF/Induct/Acc.thy	Sat Mar 13 16:37:15 2010 +0100
    77.2 +++ b/src/ZF/Induct/Acc.thy	Sat Mar 13 16:44:12 2010 +0100
    77.3 @@ -1,5 +1,4 @@
    77.4  (*  Title:      ZF/Induct/Acc.thy
    77.5 -    ID:         $Id$
    77.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    77.7      Copyright   1994  University of Cambridge
    77.8  *)
    78.1 --- a/src/ZF/Induct/Binary_Trees.thy	Sat Mar 13 16:37:15 2010 +0100
    78.2 +++ b/src/ZF/Induct/Binary_Trees.thy	Sat Mar 13 16:44:12 2010 +0100
    78.3 @@ -1,5 +1,4 @@
    78.4  (*  Title:      ZF/Induct/Binary_Trees.thy
    78.5 -    ID:         $Id$
    78.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    78.7      Copyright   1992  University of Cambridge
    78.8  *)
    79.1 --- a/src/ZF/Induct/Brouwer.thy	Sat Mar 13 16:37:15 2010 +0100
    79.2 +++ b/src/ZF/Induct/Brouwer.thy	Sat Mar 13 16:44:12 2010 +0100
    79.3 @@ -1,5 +1,4 @@
    79.4  (*  Title:      ZF/Induct/Brouwer.thy
    79.5 -    ID:         $Id$
    79.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    79.7      Copyright   1994  University of Cambridge
    79.8  *)
    80.1 --- a/src/ZF/Induct/Datatypes.thy	Sat Mar 13 16:37:15 2010 +0100
    80.2 +++ b/src/ZF/Induct/Datatypes.thy	Sat Mar 13 16:44:12 2010 +0100
    80.3 @@ -1,5 +1,4 @@
    80.4  (*  Title:      ZF/Induct/Datatypes.thy
    80.5 -    ID:         $Id$
    80.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    80.7      Copyright   1994  University of Cambridge
    80.8  *)
    81.1 --- a/src/ZF/Induct/ListN.thy	Sat Mar 13 16:37:15 2010 +0100
    81.2 +++ b/src/ZF/Induct/ListN.thy	Sat Mar 13 16:44:12 2010 +0100
    81.3 @@ -1,5 +1,4 @@
    81.4  (*  Title:      ZF/Induct/ListN.thy
    81.5 -    ID:         $Id$
    81.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    81.7      Copyright   1994  University of Cambridge
    81.8  *)
    82.1 --- a/src/ZF/Induct/Mutil.thy	Sat Mar 13 16:37:15 2010 +0100
    82.2 +++ b/src/ZF/Induct/Mutil.thy	Sat Mar 13 16:44:12 2010 +0100
    82.3 @@ -1,5 +1,4 @@
    82.4  (*  Title:      ZF/Induct/Mutil.thy
    82.5 -    ID:         $Id$
    82.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    82.7      Copyright   1996  University of Cambridge
    82.8  *)
    83.1 --- a/src/ZF/Induct/Ntree.thy	Sat Mar 13 16:37:15 2010 +0100
    83.2 +++ b/src/ZF/Induct/Ntree.thy	Sat Mar 13 16:44:12 2010 +0100
    83.3 @@ -1,5 +1,4 @@
    83.4  (*  Title:      ZF/Induct/Ntree.thy
    83.5 -    ID:         $Id$
    83.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    83.7      Copyright   1994  University of Cambridge
    83.8  *)
    84.1 --- a/src/ZF/Induct/Primrec.thy	Sat Mar 13 16:37:15 2010 +0100
    84.2 +++ b/src/ZF/Induct/Primrec.thy	Sat Mar 13 16:44:12 2010 +0100
    84.3 @@ -1,5 +1,4 @@
    84.4  (*  Title:      ZF/Induct/Primrec.thy
    84.5 -    ID:         $Id$
    84.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    84.7      Copyright   1994  University of Cambridge
    84.8  *)
    85.1 --- a/src/ZF/Induct/PropLog.thy	Sat Mar 13 16:37:15 2010 +0100
    85.2 +++ b/src/ZF/Induct/PropLog.thy	Sat Mar 13 16:44:12 2010 +0100
    85.3 @@ -1,5 +1,4 @@
    85.4  (*  Title:      ZF/Induct/PropLog.thy
    85.5 -    ID:         $Id$
    85.6      Author:     Tobias Nipkow & Lawrence C Paulson
    85.7      Copyright   1993  University of Cambridge
    85.8  *)
    86.1 --- a/src/ZF/Induct/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    86.2 +++ b/src/ZF/Induct/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    86.3 @@ -1,5 +1,4 @@
    86.4  (*  Title:      ZF/Induct/ROOT.ML
    86.5 -    ID:         $Id$
    86.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    86.7      Copyright   2001  University of Cambridge
    86.8  
    87.1 --- a/src/ZF/Induct/Rmap.thy	Sat Mar 13 16:37:15 2010 +0100
    87.2 +++ b/src/ZF/Induct/Rmap.thy	Sat Mar 13 16:44:12 2010 +0100
    87.3 @@ -1,5 +1,4 @@
    87.4  (*  Title:      ZF/Induct/Rmap.thy
    87.5 -    ID:         $Id$
    87.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    87.7      Copyright   1994  University of Cambridge
    87.8  *)
    88.1 --- a/src/ZF/Induct/Term.thy	Sat Mar 13 16:37:15 2010 +0100
    88.2 +++ b/src/ZF/Induct/Term.thy	Sat Mar 13 16:44:12 2010 +0100
    88.3 @@ -1,5 +1,4 @@
    88.4  (*  Title:      ZF/Induct/Term.thy
    88.5 -    ID:         $Id$
    88.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    88.7      Copyright   1994  University of Cambridge
    88.8  *)
    89.1 --- a/src/ZF/Induct/Tree_Forest.thy	Sat Mar 13 16:37:15 2010 +0100
    89.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Sat Mar 13 16:44:12 2010 +0100
    89.3 @@ -1,5 +1,4 @@
    89.4  (*  Title:      ZF/Induct/Tree_Forest.thy
    89.5 -    ID:         $Id$
    89.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    89.7      Copyright   1994  University of Cambridge
    89.8  *)
    90.1 --- a/src/ZF/Main.thy	Sat Mar 13 16:37:15 2010 +0100
    90.2 +++ b/src/ZF/Main.thy	Sat Mar 13 16:44:12 2010 +0100
    90.3 @@ -1,5 +1,3 @@
    90.4 -(* $Id$ *)
    90.5 -
    90.6  theory Main 
    90.7  imports Main_ZF
    90.8  begin
    91.1 --- a/src/ZF/Main_ZFC.thy	Sat Mar 13 16:37:15 2010 +0100
    91.2 +++ b/src/ZF/Main_ZFC.thy	Sat Mar 13 16:44:12 2010 +0100
    91.3 @@ -1,5 +1,4 @@
    91.4 -(* $Id$ *)
    91.5 -
    91.6 -theory Main_ZFC imports Main_ZF InfDatatype begin
    91.7 +theory Main_ZFC imports Main_ZF InfDatatype
    91.8 +begin
    91.9  
   91.10  end
    92.1 --- a/src/ZF/OrderArith.thy	Sat Mar 13 16:37:15 2010 +0100
    92.2 +++ b/src/ZF/OrderArith.thy	Sat Mar 13 16:44:12 2010 +0100
    92.3 @@ -1,8 +1,6 @@
    92.4  (*  Title:      ZF/OrderArith.thy
    92.5 -    ID:         $Id$
    92.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    92.7      Copyright   1994  University of Cambridge
    92.8 -
    92.9  *)
   92.10  
   92.11  header{*Combining Orderings: Foundations of Ordinal Arithmetic*}
    93.1 --- a/src/ZF/Ordinal.thy	Sat Mar 13 16:37:15 2010 +0100
    93.2 +++ b/src/ZF/Ordinal.thy	Sat Mar 13 16:44:12 2010 +0100
    93.3 @@ -1,8 +1,6 @@
    93.4  (*  Title:      ZF/Ordinal.thy
    93.5 -    ID:         $Id$
    93.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    93.7      Copyright   1994  University of Cambridge
    93.8 -
    93.9  *)
   93.10  
   93.11  header{*Transitive Sets and Ordinals*}
    94.1 --- a/src/ZF/QPair.thy	Sat Mar 13 16:37:15 2010 +0100
    94.2 +++ b/src/ZF/QPair.thy	Sat Mar 13 16:44:12 2010 +0100
    94.3 @@ -1,12 +1,11 @@
    94.4 -(*  Title:      ZF/qpair.thy
    94.5 -    ID:         $Id$
    94.6 +(*  Title:      ZF/QPair.thy
    94.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    94.8      Copyright   1993  University of Cambridge
    94.9  
   94.10  Many proofs are borrowed from pair.thy and sum.thy
   94.11  
   94.12  Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
   94.13 -    is not a limit ordinal? 
   94.14 +is not a limit ordinal? 
   94.15  *)
   94.16  
   94.17  header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
    95.1 --- a/src/ZF/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
    95.2 +++ b/src/ZF/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
    95.3 @@ -1,5 +1,4 @@
    95.4  (*  Title:      ZF/ROOT.ML
    95.5 -    ID:         $Id$
    95.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    95.7      Copyright   1993  University of Cambridge
    95.8  
    96.1 --- a/src/ZF/Resid/Confluence.thy	Sat Mar 13 16:37:15 2010 +0100
    96.2 +++ b/src/ZF/Resid/Confluence.thy	Sat Mar 13 16:44:12 2010 +0100
    96.3 @@ -1,8 +1,6 @@
    96.4 -(*  Title:      Confluence.thy
    96.5 -    ID:         $Id$
    96.6 +(*  Title:      ZF/Resid/Confluence.thy
    96.7      Author:     Ole Rasmussen
    96.8      Copyright   1995  University of Cambridge
    96.9 -    Logic Image: ZF
   96.10  *)
   96.11  
   96.12  theory Confluence imports Reduction begin
    97.1 --- a/src/ZF/Resid/Reduction.thy	Sat Mar 13 16:37:15 2010 +0100
    97.2 +++ b/src/ZF/Resid/Reduction.thy	Sat Mar 13 16:44:12 2010 +0100
    97.3 @@ -1,8 +1,6 @@
    97.4 -(*  Title:      Reduction.thy
    97.5 -    ID:         $Id$
    97.6 +(*  Title:      ZF/Resid/Reduction.thy
    97.7      Author:     Ole Rasmussen
    97.8      Copyright   1995  University of Cambridge
    97.9 -    Logic Image: ZF
   97.10  *)
   97.11  
   97.12  theory Reduction imports Residuals begin
    98.1 --- a/src/ZF/Resid/Residuals.thy	Sat Mar 13 16:37:15 2010 +0100
    98.2 +++ b/src/ZF/Resid/Residuals.thy	Sat Mar 13 16:44:12 2010 +0100
    98.3 @@ -1,9 +1,6 @@
    98.4 -(*  Title:      Residuals.thy
    98.5 -    ID:         $Id$
    98.6 +(*  Title:      ZF/Resid/Residuals.thy
    98.7      Author:     Ole Rasmussen
    98.8      Copyright   1995  University of Cambridge
    98.9 -    Logic Image: ZF
   98.10 -
   98.11  *)
   98.12  
   98.13  theory Residuals imports Substitution begin
    99.1 --- a/src/ZF/Tools/cartprod.ML	Sat Mar 13 16:37:15 2010 +0100
    99.2 +++ b/src/ZF/Tools/cartprod.ML	Sat Mar 13 16:44:12 2010 +0100
    99.3 @@ -1,11 +1,10 @@
    99.4  (*  Title:      ZF/Tools/cartprod.ML
    99.5 -    ID:         $Id$
    99.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    99.7      Copyright   1996  University of Cambridge
    99.8  
    99.9 -Signatures for inductive definitions
   99.10 +Signatures for inductive definitions.
   99.11  
   99.12 -Syntactic operations for Cartesian Products
   99.13 +Syntactic operations for Cartesian Products.
   99.14  *)
   99.15  
   99.16  signature FP =          (** Description of a fixed point operator **)
   100.1 --- a/src/ZF/Tools/ind_cases.ML	Sat Mar 13 16:37:15 2010 +0100
   100.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Mar 13 16:44:12 2010 +0100
   100.3 @@ -1,5 +1,4 @@
   100.4  (*  Title:      ZF/Tools/ind_cases.ML
   100.5 -    ID:         $Id$
   100.6      Author:     Markus Wenzel, LMU Muenchen
   100.7  
   100.8  Generic inductive cases facility for (co)inductive definitions.
   101.1 --- a/src/ZF/Tools/twos_compl.ML	Sat Mar 13 16:37:15 2010 +0100
   101.2 +++ b/src/ZF/Tools/twos_compl.ML	Sat Mar 13 16:44:12 2010 +0100
   101.3 @@ -1,5 +1,4 @@
   101.4  (*  Title:      ZF/Tools/twos_compl.ML
   101.5 -    ID:         $Id$
   101.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   101.7      Copyright   1993  University of Cambridge
   101.8  
   102.1 --- a/src/ZF/Trancl.thy	Sat Mar 13 16:37:15 2010 +0100
   102.2 +++ b/src/ZF/Trancl.thy	Sat Mar 13 16:44:12 2010 +0100
   102.3 @@ -1,8 +1,6 @@
   102.4  (*  Title:      ZF/Trancl.thy
   102.5 -    ID:         $Id$
   102.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   102.7      Copyright   1992  University of Cambridge
   102.8 -
   102.9  *)
  102.10  
  102.11  header{*Relations: Their General Properties and Transitive Closure*}
   103.1 --- a/src/ZF/UNITY/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
   103.2 +++ b/src/ZF/UNITY/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
   103.3 @@ -1,5 +1,4 @@
   103.4  (*  Title:      ZF/UNITY/ROOT.ML
   103.5 -    ID:         $Id$
   103.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   103.7      Copyright   1998  University of Cambridge
   103.8  
   104.1 --- a/src/ZF/WF.thy	Sat Mar 13 16:37:15 2010 +0100
   104.2 +++ b/src/ZF/WF.thy	Sat Mar 13 16:44:12 2010 +0100
   104.3 @@ -1,5 +1,4 @@
   104.4  (*  Title:      ZF/WF.thy
   104.5 -    ID:         $Id$
   104.6      Author:     Tobias Nipkow and Lawrence C Paulson
   104.7      Copyright   1994  University of Cambridge
   104.8  
   105.1 --- a/src/ZF/equalities.thy	Sat Mar 13 16:37:15 2010 +0100
   105.2 +++ b/src/ZF/equalities.thy	Sat Mar 13 16:44:12 2010 +0100
   105.3 @@ -1,8 +1,6 @@
   105.4 -(*  Title:      ZF/equalities
   105.5 -    ID:         $Id$
   105.6 +(*  Title:      ZF/equalities.thy
   105.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   105.8      Copyright   1992  University of Cambridge
   105.9 -
  105.10  *)
  105.11  
  105.12  header{*Basic Equalities and Inclusions*}
   106.1 --- a/src/ZF/ex/BinEx.thy	Sat Mar 13 16:37:15 2010 +0100
   106.2 +++ b/src/ZF/ex/BinEx.thy	Sat Mar 13 16:44:12 2010 +0100
   106.3 @@ -1,9 +1,8 @@
   106.4 -(*  Title:      ZF/ex/BinEx.ML
   106.5 -    ID:         $Id$
   106.6 +(*  Title:      ZF/ex/BinEx.thy
   106.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   106.8      Copyright   1994  University of Cambridge
   106.9  
  106.10 -Examples of performing binary arithmetic by simplification
  106.11 +Examples of performing binary arithmetic by simplification.
  106.12  *)
  106.13  
  106.14  theory BinEx imports Main begin
   107.1 --- a/src/ZF/ex/CoUnit.thy	Sat Mar 13 16:37:15 2010 +0100
   107.2 +++ b/src/ZF/ex/CoUnit.thy	Sat Mar 13 16:44:12 2010 +0100
   107.3 @@ -1,5 +1,4 @@
   107.4 -(*  Title:      ZF/ex/CoUnit.ML
   107.5 -    ID:         $Id$
   107.6 +(*  Title:      ZF/ex/CoUnit.thy
   107.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   107.8      Copyright   1994  University of Cambridge
   107.9  *)
   108.1 --- a/src/ZF/ex/Commutation.thy	Sat Mar 13 16:37:15 2010 +0100
   108.2 +++ b/src/ZF/ex/Commutation.thy	Sat Mar 13 16:44:12 2010 +0100
   108.3 @@ -1,10 +1,8 @@
   108.4  (*  Title:      HOL/Lambda/Commutation.thy
   108.5 -    ID:         $Id$
   108.6      Author:     Tobias Nipkow & Sidi Ould Ehmety
   108.7      Copyright   1995  TU Muenchen
   108.8  
   108.9 -Commutation theory for proving the Church Rosser theorem
  108.10 -        ported from Isabelle/HOL  by Sidi Ould Ehmety
  108.11 +Commutation theory for proving the Church Rosser theorem.
  108.12  *)
  108.13  
  108.14  theory Commutation imports Main begin
   109.1 --- a/src/ZF/ex/NatSum.thy	Sat Mar 13 16:37:15 2010 +0100
   109.2 +++ b/src/ZF/ex/NatSum.thy	Sat Mar 13 16:44:12 2010 +0100
   109.3 @@ -1,5 +1,4 @@
   109.4  (*  Title:      ZF/ex/Natsum.thy
   109.5 -    ID:         $Id$
   109.6      Author:     Tobias Nipkow & Lawrence C Paulson
   109.7  
   109.8  A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
   110.1 --- a/src/ZF/ex/ROOT.ML	Sat Mar 13 16:37:15 2010 +0100
   110.2 +++ b/src/ZF/ex/ROOT.ML	Sat Mar 13 16:44:12 2010 +0100
   110.3 @@ -1,5 +1,4 @@
   110.4  (*  Title:      ZF/ex/ROOT.ML
   110.5 -    ID:         $Id$
   110.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   110.7      Copyright   1993  University of Cambridge
   110.8  
   111.1 --- a/src/ZF/ex/Ramsey.thy	Sat Mar 13 16:37:15 2010 +0100
   111.2 +++ b/src/ZF/ex/Ramsey.thy	Sat Mar 13 16:44:12 2010 +0100
   111.3 @@ -1,5 +1,4 @@
   111.4 -(*  Title:      ZF/ex/ramsey.thy
   111.5 -    ID:         $Id$
   111.6 +(*  Title:      ZF/ex/Ramsey.thy
   111.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   111.8      Copyright   1992  University of Cambridge
   111.9  
  111.10 @@ -23,7 +22,6 @@
  111.11  fun ram 0 j = 1
  111.12    | ram i 0 = 1
  111.13    | ram i j = ram (i-1) j + ram i (j-1)
  111.14 -
  111.15  *)
  111.16  
  111.17  theory Ramsey imports Main begin
   112.1 --- a/src/ZF/ex/misc.thy	Sat Mar 13 16:37:15 2010 +0100
   112.2 +++ b/src/ZF/ex/misc.thy	Sat Mar 13 16:44:12 2010 +0100
   112.3 @@ -1,5 +1,4 @@
   112.4 -(*  Title:      ZF/ex/misc.ML
   112.5 -    ID:         $Id$
   112.6 +(*  Title:      ZF/ex/misc.thy
   112.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   112.8      Copyright   1993  University of Cambridge
   112.9  
   113.1 --- a/src/ZF/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
   113.2 +++ b/src/ZF/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
   113.3 @@ -1,9 +1,8 @@
   113.4 -(*  Title:      ZF/simpdata
   113.5 -    ID:         $Id$
   113.6 +(*  Title:      ZF/simpdata.ML
   113.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   113.8      Copyright   1991  University of Cambridge
   113.9  
  113.10 -Rewriting for ZF set theory: specialized extraction of rewrites from theorems
  113.11 +Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
  113.12  *)
  113.13  
  113.14  (*** New version of mk_rew_rules ***)