# HG changeset patch
# User wenzelm
# Date 1001622496 -7200
# Node ID 3f3d1add4d94bbf532a19a3cb7deedffe4ee1eec
# Parent  c760ea8154ee81fad2b76d331e37f5262f1efb3d
eliminated theories "equalities" and "mono" (made part of "Typedef",
  which supercedes "subset");

diff -r c760ea8154ee -r 3f3d1add4d94 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 27 22:26:00 2001 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 27 22:28:16 2001 +0200
@@ -6,7 +6,7 @@
 Notions about functions.
 *)
 
-Fun = Inverse_Image + equalities + 
+Fun = Inverse_Image + Typedef + 
 
 instance set :: (term) order
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
diff -r c760ea8154ee -r 3f3d1add4d94 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 27 22:26:00 2001 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 27 22:28:16 2001 +0200
@@ -103,11 +103,11 @@
   Tools/primrec_package.ML Tools/recdef_package.ML \
   Tools/record_package.ML Tools/split_rule.ML \
   Tools/svc_funcs.ML Tools/typedef_package.ML \
-  Transitive_Closure.thy Transitive_Closure_lemmas.ML Wellfounded_Recursion.ML \
-  Wellfounded_Recursion.thy Wellfounded_Relations.ML \
+  Transitive_Closure.thy Transitive_Closure_lemmas.ML Typedef.thy \
+  Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
-  equalities.ML equalities.thy hologic.ML meson_lemmas.ML mono.ML \
-  mono.thy simpdata.ML subset.ML subset.thy thy_syntax.ML
+  equalities.ML hologic.ML meson_lemmas.ML mono.ML \
+  simpdata.ML subset.ML thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
diff -r c760ea8154ee -r 3f3d1add4d94 src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Thu Sep 27 22:26:00 2001 +0200
+++ b/src/HOL/Lfp.thy	Thu Sep 27 22:28:16 2001 +0200
@@ -6,7 +6,7 @@
 The Knaster-Tarski Theorem
 *)
 
-Lfp = mono + Product_Type +
+Lfp = Product_Type +
 
 constdefs
   lfp :: ['a set=>'a set] => 'a set
diff -r c760ea8154ee -r 3f3d1add4d94 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Sep 27 22:26:00 2001 +0200
+++ b/src/HOL/SetInterval.thy	Thu Sep 27 22:28:16 2001 +0200
@@ -6,19 +6,19 @@
 lessThan, greaterThan, atLeast, atMost
 *)
 
-SetInterval = equalities + NatArith + 
+SetInterval = NatArith + 
 
 constdefs
- lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
-"{..u(} == {x. x<u}"
+  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
+  "{..u(} == {x. x<u}"
 
- atMost      :: "('a::ord) => 'a set"	("(1{.._})")
-"{..u} == {x. x<=u}"
+  atMost      :: "('a::ord) => 'a set"	("(1{.._})")
+  "{..u} == {x. x<=u}"
 
- greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
-"{)l..} == {x. l<x}"
+  greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
+  "{)l..} == {x. l<x}"
 
- atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
-"{l..} == {x. l<=x}"
+  atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
+  "{l..} == {x. l<=x}"
 
 end
diff -r c760ea8154ee -r 3f3d1add4d94 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Thu Sep 27 22:26:00 2001 +0200
+++ b/src/HOL/Sum_Type.thy	Thu Sep 27 22:28:16 2001 +0200
@@ -6,7 +6,7 @@
 The disjoint sum of two types.
 *)
 
-Sum_Type = mono + Product_Type +
+Sum_Type = Product_Type +
 
 (* type definition *)
 
diff -r c760ea8154ee -r 3f3d1add4d94 src/HOL/equalities.thy
--- a/src/HOL/equalities.thy	Thu Sep 27 22:26:00 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*  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 c760ea8154ee -r 3f3d1add4d94 src/HOL/mono.thy
--- a/src/HOL/mono.thy	Thu Sep 27 22:26:00 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*  Title:      HOL/mono.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-*)
-
-mono = equalities