more precise headers;
authorwenzelm
Fri Feb 18 16:22:27 2011 +0100 (2011-02-18)
changeset 417771f7cbe39d425
parent 41776 3bd83302a3c3
child 41778 5f79a9e42507
more precise headers;
src/FOL/ex/If.thy
src/FOL/ex/Quantifiers_Cla.thy
src/FOLP/ex/Foundation.thy
src/FOLP/ex/Nat.thy
src/HOL/ZF/Games.thy
src/ZF/AC/AC17_AC1.thy
src/ZF/ArithSimp.thy
src/ZF/Bool.thy
src/ZF/Datatype_ZF.thy
src/ZF/Int_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/Sum.thy
src/ZF/ex/Commutation.thy
src/ZF/ex/NatSum.thy
src/ZF/pair.thy
     1.1 --- a/src/FOL/ex/If.thy	Fri Feb 18 16:11:58 2011 +0100
     1.2 +++ b/src/FOL/ex/If.thy	Fri Feb 18 16:22:27 2011 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      FOL/ex/If.ML
     1.5 +(*  Title:      FOL/ex/If.thy
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1991  University of Cambridge
     1.8  *)
     2.1 --- a/src/FOL/ex/Quantifiers_Cla.thy	Fri Feb 18 16:11:58 2011 +0100
     2.2 +++ b/src/FOL/ex/Quantifiers_Cla.thy	Fri Feb 18 16:22:27 2011 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      FOL/ex/Quantifiers_Int.thy
     2.5 +(*  Title:      FOL/ex/Quantifiers_Cla.thy
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   1991  University of Cambridge
     2.8  *)
     3.1 --- a/src/FOLP/ex/Foundation.thy	Fri Feb 18 16:11:58 2011 +0100
     3.2 +++ b/src/FOLP/ex/Foundation.thy	Fri Feb 18 16:22:27 2011 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      FOLP/ex/Foundation.ML
     3.5 +(*  Title:      FOLP/ex/Foundation.thy
     3.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7      Copyright   1991  University of Cambridge
     3.8  *)
     4.1 --- a/src/FOLP/ex/Nat.thy	Fri Feb 18 16:11:58 2011 +0100
     4.2 +++ b/src/FOLP/ex/Nat.thy	Fri Feb 18 16:22:27 2011 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      FOLP/ex/nat.thy
     4.5 +(*  Title:      FOLP/ex/Nat.thy
     4.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7      Copyright   1992  University of Cambridge
     4.8  *)
     5.1 --- a/src/HOL/ZF/Games.thy	Fri Feb 18 16:11:58 2011 +0100
     5.2 +++ b/src/HOL/ZF/Games.thy	Fri Feb 18 16:22:27 2011 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/ZF/MainZF.thy/Games.thy
     5.5 +(*  Title:      HOL/ZF/Games.thy
     5.6      Author:     Steven Obua
     5.7  
     5.8  An application of HOLZF: Partizan Games.  See "Partizan Games in
     6.1 --- a/src/ZF/AC/AC17_AC1.thy	Fri Feb 18 16:11:58 2011 +0100
     6.2 +++ b/src/ZF/AC/AC17_AC1.thy	Fri Feb 18 16:22:27 2011 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      ZF/AC/AC1_AC17.thy
     6.5 +(*  Title:      ZF/AC/AC17_AC1.thy
     6.6      Author:     Krzysztof Grabczewski
     6.7  
     6.8  The equivalence of AC0, AC1 and AC17
     7.1 --- a/src/ZF/ArithSimp.thy	Fri Feb 18 16:11:58 2011 +0100
     7.2 +++ b/src/ZF/ArithSimp.thy	Fri Feb 18 16:22:27 2011 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      ZF/ArithSimp.ML
     7.5 +(*  Title:      ZF/ArithSimp.thy
     7.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7      Copyright   2000  University of Cambridge
     7.8  *)
     8.1 --- a/src/ZF/Bool.thy	Fri Feb 18 16:11:58 2011 +0100
     8.2 +++ b/src/ZF/Bool.thy	Fri Feb 18 16:22:27 2011 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      ZF/bool.thy
     8.5 +(*  Title:      ZF/Bool.thy
     8.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7      Copyright   1992  University of Cambridge
     8.8  *)
     9.1 --- a/src/ZF/Datatype_ZF.thy	Fri Feb 18 16:11:58 2011 +0100
     9.2 +++ b/src/ZF/Datatype_ZF.thy	Fri Feb 18 16:22:27 2011 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      ZF/Datatype.thy
     9.5 +(*  Title:      ZF/Datatype_ZF.thy
     9.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7      Copyright   1997  University of Cambridge
     9.8  *)
    10.1 --- a/src/ZF/Int_ZF.thy	Fri Feb 18 16:11:58 2011 +0100
    10.2 +++ b/src/ZF/Int_ZF.thy	Fri Feb 18 16:22:27 2011 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      ZF/Int.thy
    10.5 +(*  Title:      ZF/Int_ZF.thy
    10.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7      Copyright   1993  University of Cambridge
    10.8  *)
    11.1 --- a/src/ZF/OrdQuant.thy	Fri Feb 18 16:11:58 2011 +0100
    11.2 +++ b/src/ZF/OrdQuant.thy	Fri Feb 18 16:22:27 2011 +0100
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      ZF/AC/OrdQuant.thy
    11.5 +(*  Title:      ZF/OrdQuant.thy
    11.6      Authors:    Krzysztof Grabczewski and L C Paulson
    11.7  *)
    11.8  
    12.1 --- a/src/ZF/Sum.thy	Fri Feb 18 16:11:58 2011 +0100
    12.2 +++ b/src/ZF/Sum.thy	Fri Feb 18 16:22:27 2011 +0100
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      ZF/sum.thy
    12.5 +(*  Title:      ZF/Sum.thy
    12.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7      Copyright   1993  University of Cambridge
    12.8  *)
    13.1 --- a/src/ZF/ex/Commutation.thy	Fri Feb 18 16:11:58 2011 +0100
    13.2 +++ b/src/ZF/ex/Commutation.thy	Fri Feb 18 16:22:27 2011 +0100
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/Lambda/Commutation.thy
    13.5 +(*  Title:      ZF/ex/Commutation.thy
    13.6      Author:     Tobias Nipkow & Sidi Ould Ehmety
    13.7      Copyright   1995  TU Muenchen
    13.8  
    14.1 --- a/src/ZF/ex/NatSum.thy	Fri Feb 18 16:11:58 2011 +0100
    14.2 +++ b/src/ZF/ex/NatSum.thy	Fri Feb 18 16:22:27 2011 +0100
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      ZF/ex/Natsum.thy
    14.5 +(*  Title:      ZF/ex/NatSum.thy
    14.6      Author:     Tobias Nipkow & Lawrence C Paulson
    14.7  
    14.8  A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
    15.1 --- a/src/ZF/pair.thy	Fri Feb 18 16:11:58 2011 +0100
    15.2 +++ b/src/ZF/pair.thy	Fri Feb 18 16:22:27 2011 +0100
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      ZF/pair
    15.5 +(*  Title:      ZF/pair.thy
    15.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7      Copyright   1992  University of Cambridge
    15.8