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.
merged.
authorhuffman
Thu, 18 Dec 2008 09:30:36 -0800
changeset 29139 6e0b7b114072
parent 29138 661a8db7e647 (diff)
parent 29137 295b35b7a202 (current diff)
child 29140 e7ac5bb20aed
child 29141 d5582ab1311f
child 29681 4374ca526b65
merged.
--- a/src/HOLCF/Adm.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Adm.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Adm.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
 *)
 
--- a/src/HOLCF/Algebraic.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Algebraic.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Algebraic.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Bifinite.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Bifinite.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Bifinite.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Cfun.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Cfun.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 
 Definition of the type ->  of continuous functions.
--- a/src/HOLCF/CompactBasis.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/CompactBasis.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Completion.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Completion.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Completion.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Cont.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Cont.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Cont.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Results about continuity and monotonicity.
 *)
 
 header {* Continuity and monotonicity *}
--- a/src/HOLCF/ConvexPD.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/ConvexPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Cprod.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Cprod.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Partial ordering for cartesian product of HOL products.
 *)
 
 header {* The cpo of cartesian products *}
--- a/src/HOLCF/Deflation.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Deflation.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Deflation.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Discrete.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Discrete.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
-
-Discrete CPOs.
 *)
 
 header {* Discrete cpo types *}
--- a/src/HOLCF/Domain.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Domain.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Domain.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Ffun.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,10 +1,5 @@
 (*  Title:      HOLCF/FunCpo.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Definition of the partial ordering for the type of all functions => (fun)
-
-Class instance of  => (fun) for class pcpo.
 *)
 
 header {* Class instances for the full function space *}
--- a/src/HOLCF/Fix.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Fix.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Fix.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Definitions for fixed point operator and admissibility.
 *)
 
 header {* Fixed point operator and admissibility *}
--- a/src/HOLCF/Fixrec.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Fixrec.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Fixrec.thy
-    ID:         $Id$
     Author:     Amber Telfer and Brian Huffman
 *)
 
--- a/src/HOLCF/HOLCF.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/HOLCF.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/HOLCF.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 
 HOLCF -- a semantic extension of HOL by the LCF logic.
--- a/src/HOLCF/Lift.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Lift.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Lift.thy
-    ID:         $Id$
     Author:     Olaf Mueller
 *)
 
--- a/src/HOLCF/LowerPD.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/LowerPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/One.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/One.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/One.thy
-    ID:         $Id$
     Author:     Oscar Slotosch
-
-The unit domain.
 *)
 
 header {* The unit domain *}
--- a/src/HOLCF/Pcpo.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Pcpo.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 *)
 
--- a/src/HOLCF/Pcpodef.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Pcpodef.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Porder.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Porder.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Porder.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
 *)
 
--- a/src/HOLCF/Sprod.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Sprod.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Sprod.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-
-Strict product with typedef.
 *)
 
 header {* The type of strict products *}
--- a/src/HOLCF/Ssum.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Ssum.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-
-Strict sum with typedef.
 *)
 
 header {* The type of strict sums *}
--- a/src/HOLCF/Tr.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Tr.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Tr.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
 *)
 
 header {* The type of lifted booleans *}
--- a/src/HOLCF/Universal.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Universal.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Universal.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
--- a/src/HOLCF/Up.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/Up.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Up.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-
-Lifting.
 *)
 
 header {* The type of lifted values *}
--- a/src/HOLCF/UpperPD.thy	Wed Dec 17 14:40:04 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Thu Dec 18 09:30:36 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/UpperPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
isabelle