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.
dropped ID
authorhaftmann
Wed, 21 Jan 2009 16:47:31 +0100
changeset 29580 117b88da143c
parent 29579 cb520b766e00
child 29581 b3b33e0298eb
dropped ID
src/HOL/ATP_Linkup.thy file | annotate | diff | comparison | revisions
src/HOL/Datatype.thy file | annotate | diff | comparison | revisions
src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
src/HOL/FunDef.thy file | annotate | diff | comparison | revisions
src/HOL/Lattices.thy file | annotate | diff | comparison | revisions
src/HOL/Orderings.thy file | annotate | diff | comparison | revisions
src/HOL/Wellfounded.thy file | annotate | diff | comparison | revisions
src/Pure/primitive_defs.ML file | annotate | diff | comparison | revisions
src/ZF/Inductive_ZF.thy file | annotate | diff | comparison | revisions
src/ZF/Main_ZF.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ATP_Linkup.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ATP_Linkup.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson
     Author:     Jia Meng, NICTA
     Author:     Fabian Immler, TUM
--- a/src/HOL/Datatype.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Datatype.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Datatype.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 
--- a/src/HOL/Finite_Set.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Finite_Set.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
                 with contributions by Jeremy Avigad
 *)
--- a/src/HOL/FunDef.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/FunDef.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/FunDef.thy
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 *)
 
--- a/src/HOL/Lattices.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Lattices.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lattices.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
 *)
 
--- a/src/HOL/Orderings.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Orderings.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Orderings.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
--- a/src/HOL/Wellfounded.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
-(*  ID:         $Id$
-    Author:     Tobias Nipkow
+(*  Author:     Tobias Nipkow
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Konrad Slind, Alexander Krauss
     Copyright   1992-2008  University of Cambridge and TU Muenchen
--- a/src/Pure/primitive_defs.ML	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/Pure/primitive_defs.ML	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/primitive_defs.ML
-    ID:         $Id$
     Author:     Makarius
 
 Primitive definition forms.
--- a/src/ZF/Inductive_ZF.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/ZF/Inductive_ZF.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Inductive_ZF.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
--- a/src/ZF/Main_ZF.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/ZF/Main_ZF.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,3 @@
-(*$Id$*)
-
 header{*Theory Main: Everything Except AC*}
 
 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
isabelle