src/HOL/Typedef.thy
changeset 11770 b6bb7a853dd2
parent 11743 b9739c85dd44
child 11979 0a3dace545c5
     1.1 --- a/src/HOL/Typedef.thy	Sun Oct 14 22:07:01 2001 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Sun Oct 14 22:08:29 2001 +0200
     1.3 @@ -8,6 +8,9 @@
     1.4  theory Typedef = Set
     1.5  files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
     1.6  
     1.7 +(*belongs to theory Set*)
     1.8 +declare atomize_ball [symmetric, rulify]
     1.9 +
    1.10  (* Courtesy of Stephan Merz *)
    1.11  lemma Least_mono: 
    1.12    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    1.13 @@ -20,10 +23,6 @@
    1.14    done
    1.15  
    1.16  
    1.17 -(*belongs to theory Set*)
    1.18 -setup Rulify.setup
    1.19 -
    1.20 -
    1.21  subsection {* HOL type definitions *}
    1.22  
    1.23  constdefs