Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more precise headers;
authorwenzelm
Fri, 18 Feb 2011 16:22:27 +0100
changeset 41777 1f7cbe39d425
parent 41776 3bd83302a3c3
child 41778 5f79a9e42507
more precise headers;
src/FOL/ex/If.thy file | annotate | diff | comparison | revisions
src/FOL/ex/Quantifiers_Cla.thy file | annotate | diff | comparison | revisions
src/FOLP/ex/Foundation.thy file | annotate | diff | comparison | revisions
src/FOLP/ex/Nat.thy file | annotate | diff | comparison | revisions
src/HOL/ZF/Games.thy file | annotate | diff | comparison | revisions
src/ZF/AC/AC17_AC1.thy file | annotate | diff | comparison | revisions
src/ZF/ArithSimp.thy file | annotate | diff | comparison | revisions
src/ZF/Bool.thy file | annotate | diff | comparison | revisions
src/ZF/Datatype_ZF.thy file | annotate | diff | comparison | revisions
src/ZF/Int_ZF.thy file | annotate | diff | comparison | revisions
src/ZF/OrdQuant.thy file | annotate | diff | comparison | revisions
src/ZF/Sum.thy file | annotate | diff | comparison | revisions
src/ZF/ex/Commutation.thy file | annotate | diff | comparison | revisions
src/ZF/ex/NatSum.thy file | annotate | diff | comparison | revisions
src/ZF/pair.thy file | annotate | diff | comparison | revisions 
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
--- 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
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
--- 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
 *)
 
--- 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
 *)
--- 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
 
--- 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.
--- 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
isabelle