# 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 'a set" ("(1{.._'(})") + "{..u(} == {x. x '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 'a set" ("(1{')_..})") + "{)l..} == {x. l '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