HOL/subset.thy, equalities.thy, mono.thy: new
HOL/Lfp.thy: now depends upon mono
HOL/Gfp.thy: depends upon Lfp, not just mono
--- 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