# HG changeset patch
# User wenzelm
# Date 1298042547 -3600
# Node ID 1f7cbe39d425d4ffd7a9d2f4d2d2556d6abb926c
# Parent  3bd83302a3c3ad99b96d59a3933430e82457138a
more precise headers;

diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/FOL/ex/If.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOL/ex/If.ML
+(*  Title:      FOL/ex/If.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/FOL/ex/Quantifiers_Cla.thy
--- a/src/FOL/ex/Quantifiers_Cla.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/FOL/ex/Quantifiers_Cla.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOL/ex/Quantifiers_Int.thy
+(*  Title:      FOL/ex/Quantifiers_Cla.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/FOLP/ex/Foundation.thy
--- a/src/FOLP/ex/Foundation.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/FOLP/ex/Foundation.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ex/Foundation.ML
+(*  Title:      FOLP/ex/Foundation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/FOLP/ex/Nat.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      FOLP/ex/nat.thy
+(*  Title:      FOLP/ex/Nat.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/HOL/ZF/Games.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ZF/MainZF.thy/Games.thy
+(*  Title:      HOL/ZF/Games.thy
     Author:     Steven Obua
 
 An application of HOLZF: Partizan Games.  See "Partizan Games in
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/AC/AC17_AC1.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/AC/AC1_AC17.thy
+(*  Title:      ZF/AC/AC17_AC1.thy
     Author:     Krzysztof Grabczewski
 
 The equivalence of AC0, AC1 and AC17
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/ArithSimp.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ArithSimp.ML
+(*  Title:      ZF/ArithSimp.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/Bool.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/bool.thy
+(*  Title:      ZF/Bool.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/Datatype_ZF.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Datatype.thy
+(*  Title:      ZF/Datatype_ZF.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/Int_ZF.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Int.thy
+(*  Title:      ZF/Int_ZF.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/OrdQuant.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/AC/OrdQuant.thy
+(*  Title:      ZF/OrdQuant.thy
     Authors:    Krzysztof Grabczewski and L C Paulson
 *)
 
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/Sum.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/sum.thy
+(*  Title:      ZF/Sum.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/ex/Commutation.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Lambda/Commutation.thy
+(*  Title:      ZF/ex/Commutation.thy
     Author:     Tobias Nipkow & Sidi Ould Ehmety
     Copyright   1995  TU Muenchen
 
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/ex/NatSum.thy
--- a/src/ZF/ex/NatSum.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/ex/NatSum.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/ex/Natsum.thy
+(*  Title:      ZF/ex/NatSum.thy
     Author:     Tobias Nipkow & Lawrence C Paulson
 
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
diff -r 3bd83302a3c3 -r 1f7cbe39d425 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Fri Feb 18 16:11:58 2011 +0100
+++ b/src/ZF/pair.thy	Fri Feb 18 16:22:27 2011 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ZF/pair
+(*  Title:      ZF/pair.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge