--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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"
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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
--- 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
*)
--- 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
--- 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
--- 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
*)
--- 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
--- 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
--- 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
--- 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
*)
--- 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
--- 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
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
*)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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*}
--- 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.
--- 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*}
--- 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*}
--- 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
--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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"];
--- 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*}
--- 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*}
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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
--- 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*}
--- 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*}
--- 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*}
--- 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
--- 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
--- 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
--- 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
--- 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 **)
--- 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.
--- 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
--- 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*}
--- 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
--- 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
--- 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*}
--- 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
--- 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
*)
--- 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
--- 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.
--- 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
--- 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
--- 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
--- 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 ***)