# HG changeset patch
# User lcp
# Date 777287456 -7200
# Node ID ab4328bbff70b9b3342aec74df1c8642efaccae5
# Parent  0ec63df3ae048771ba9c5b24a3e00d71fdad08c9
HOL/subset.thy, equalities.thy, mono.thy: new
HOL/Lfp.thy: now depends upon mono
HOL/Gfp.thy: depends upon Lfp, not just mono

diff -r 0ec63df3ae04 -r ab4328bbff70 Gfp.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 +
diff -r 0ec63df3ae04 -r ab4328bbff70 Lfp.thy
--- 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*)
diff -r 0ec63df3ae04 -r ab4328bbff70 equalities.thy
--- /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
diff -r 0ec63df3ae04 -r ab4328bbff70 mono.thy
--- /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
diff -r 0ec63df3ae04 -r ab4328bbff70 subset.thy
--- /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