# HG changeset patch
# User wenzelm
# Date 1247170198 -7200
# Node ID e81979a703a4dd274001ae7fd7a84c952f5439c4
# Parent  a89f758dba5bdca66d6f50549bb256b60ab0023e
removed obsolete CVS Ids;

diff -r a89f758dba5b -r e81979a703a4 src/FOL/FOL.thy
--- 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
 *)
 
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ROOT.ML
--- 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";
diff -r a89f758dba5b -r e81979a703a4 src/FOL/cladata.ML
--- 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
 
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Classical.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/First_Order_Logic.thy
--- 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
 *)
 
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Foundation.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/If.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Intro.thy
--- 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
 
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Intuitionistic.thy
--- 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
 
-
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Miniscope.thy
--- 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
 
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Nat.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Natural_Numbers.thy
--- 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.
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Prolog.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Propositional_Cla.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Propositional_Int.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Quantifiers_Cla.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/ex/Quantifiers_Int.thy
--- 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
 *)
diff -r a89f758dba5b -r e81979a703a4 src/FOL/fologic.ML
--- 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.
diff -r a89f758dba5b -r e81979a703a4 src/FOL/intprover.ML
--- 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
 
diff -r a89f758dba5b -r e81979a703a4 src/FOL/simpdata.ML
--- 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