HOL/subset.thy, equalities.thy, mono.thy: new
authorlcp
Fri, 19 Aug 1994 11:10:56 +0200
changeset 116 ab4328bbff70
parent 115 0ec63df3ae04
child 117 3716c99fb6a1
HOL/subset.thy, equalities.thy, mono.thy: new HOL/Lfp.thy: now depends upon mono HOL/Gfp.thy: depends upon Lfp, not just mono
Gfp.thy
Lfp.thy
equalities.thy
mono.thy
subset.thy
--- a/Gfp.thy	Fri Aug 19 11:02:45 1994 +0200
+++ b/Gfp.thy	Fri Aug 19 11:10:56 1994 +0200
@@ -1,9 +1,9 @@
 (*  Title: 	HOL/gfp.thy
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    Copyright   1994  University of Cambridge
 
-Greatest fixed points
+Greatest fixed points (requires Lfp too!)
 *)
 
 Gfp = Lfp +
--- a/Lfp.thy	Fri Aug 19 11:02:45 1994 +0200
+++ b/Lfp.thy	Fri Aug 19 11:10:56 1994 +0200
@@ -6,7 +6,7 @@
 The Knaster-Tarski Theorem
 *)
 
-Lfp = Sum +
+Lfp = mono + 
 consts lfp :: "['a set=>'a set] => 'a set"
 rules
  (*least fixed point*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/equalities.thy	Fri Aug 19 11:10:56 1994 +0200
@@ -0,0 +1,9 @@
+(*  Title: 	HOL/equalities
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Equalities involving union, intersection, inclusion, etc.
+*)
+
+equalities = subset
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/mono.thy	Fri Aug 19 11:10:56 1994 +0200
@@ -0,0 +1,8 @@
+(*  Title: 	HOL/mono
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+*)
+
+mono = subset
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/subset.thy	Fri Aug 19 11:10:56 1994 +0200
@@ -0,0 +1,7 @@
+(*  Title: 	HOL/subset.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+*)
+
+subset = Fun