removed obsolete CVS Ids;
authorwenzelm
Thu, 09 Jul 2009 22:09:58 +0200
changeset 31974 e81979a703a4
parent 31973 a89f758dba5b
child 31975 366ad09d39ef
removed obsolete CVS Ids;
src/FOL/FOL.thy
src/FOL/ROOT.ML
src/FOL/cladata.ML
src/FOL/ex/Classical.thy
src/FOL/ex/First_Order_Logic.thy
src/FOL/ex/Foundation.thy
src/FOL/ex/If.thy
src/FOL/ex/Intro.thy
src/FOL/ex/Intuitionistic.thy
src/FOL/ex/Miniscope.thy
src/FOL/ex/Nat.thy
src/FOL/ex/Natural_Numbers.thy
src/FOL/ex/Prolog.thy
src/FOL/ex/Propositional_Cla.thy
src/FOL/ex/Propositional_Int.thy
src/FOL/ex/Quantifiers_Cla.thy
src/FOL/ex/Quantifiers_Int.thy
src/FOL/fologic.ML
src/FOL/intprover.ML
src/FOL/simpdata.ML
--- a/src/FOL/FOL.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/FOL.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/FOL.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson and Markus Wenzel
 *)
 
--- a/src/FOL/ROOT.ML	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ROOT.ML	Thu Jul 09 22:09:58 2009 +0200
@@ -1,7 +1,3 @@
-(*  Title:      FOL/ROOT.ML
-    ID:         $Id$
-
-First-Order Logic with Natural Deduction.
-*)
+(* First-Order Logic with Natural Deduction *)
 
 use_thy "FOL";
--- a/src/FOL/cladata.ML	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/cladata.ML	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/cladata.ML
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1996  University of Cambridge
 
--- a/src/FOL/ex/Classical.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Classical.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      FOL/ex/Classical
-    ID:         $Id$
+(*  Title:      FOL/ex/Classical.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
--- a/src/FOL/ex/First_Order_Logic.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/First_Order_Logic.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/First_Order_Logic.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Munich
 *)
 
--- a/src/FOL/ex/Foundation.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Foundation.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      FOL/ex/Foundation.ML
-    ID:         $Id$
+(*  Title:      FOL/ex/Foundation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
--- a/src/FOL/ex/If.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/If.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/If.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
--- a/src/FOL/ex/Intro.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Intro.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Intro.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
--- a/src/FOL/ex/Intuitionistic.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Intuitionistic.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,12 +1,13 @@
-(*  Title:      FOL/ex/Intuitionistic
-    ID:         $Id$
+(*  Title:      FOL/ex/Intuitionistic.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
 
-header{*Intuitionistic First-Order Logic*}
+header {* Intuitionistic First-Order Logic *}
 
-theory Intuitionistic imports IFOL begin
+theory Intuitionistic
+imports IFOL
+begin
 
 (*
 Single-step ML commands:
@@ -422,4 +423,3 @@
 
 end
 
-
--- a/src/FOL/ex/Miniscope.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Miniscope.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Miniscope.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
--- a/src/FOL/ex/Nat.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Nat.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Nat.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
--- a/src/FOL/ex/Natural_Numbers.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Natural_Numbers.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,11 +1,12 @@
 (*  Title:      FOL/ex/Natural_Numbers.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Munich
 *)
 
 header {* Natural numbers *}
 
-theory Natural_Numbers imports FOL begin
+theory Natural_Numbers
+imports FOL
+begin
 
 text {*
   Theory of the natural numbers: Peano's axioms, primitive recursion.
--- a/src/FOL/ex/Prolog.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Prolog.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      FOL/ex/prolog.thy
-    ID:         $Id$
+(*  Title:      FOL/ex/Prolog.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
--- a/src/FOL/ex/Propositional_Cla.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Propositional_Cla.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Propositional_Cla.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
--- a/src/FOL/ex/Propositional_Int.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Propositional_Int.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Propositional_Int.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
--- a/src/FOL/ex/Quantifiers_Cla.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Quantifiers_Cla.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Quantifiers_Int.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
--- a/src/FOL/ex/Quantifiers_Int.thy	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/Quantifiers_Int.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
--- a/src/FOL/fologic.ML	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/fologic.ML	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/fologic.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson
 
 Abstract syntax operations for FOL.
--- a/src/FOL/intprover.ML	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/intprover.ML	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      FOL/int-prover
-    ID:         $Id$
+(*  Title:      FOL/intprover.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
--- a/src/FOL/simpdata.ML	Thu Jul 09 22:04:10 2009 +0200
+++ b/src/FOL/simpdata.ML	Thu Jul 09 22:09:58 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      FOL/simpdata.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge