src/HOL/Typedef.thy
changeset 11979 0a3dace545c5
parent 11770 b6bb7a853dd2
child 11982 65e2822d83dd
     1.1 --- a/src/HOL/Typedef.thy	Sun Oct 28 22:58:39 2001 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Sun Oct 28 22:59:12 2001 +0100
     1.3 @@ -3,18 +3,15 @@
     1.4      Author:     Markus Wenzel, TU Munich
     1.5  *)
     1.6  
     1.7 -header {* Set-theory lemmas and HOL type definitions *}
     1.8 +header {* HOL type definitions *}
     1.9  
    1.10  theory Typedef = Set
    1.11 -files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
    1.12 +files ("Tools/typedef_package.ML"):
    1.13  
    1.14 -(*belongs to theory Set*)
    1.15 -declare atomize_ball [symmetric, rulify]
    1.16 -
    1.17 -(* Courtesy of Stephan Merz *)
    1.18  lemma Least_mono: 
    1.19    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    1.20      ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    1.21 +    -- {* Courtesy of Stephan Merz *}
    1.22    apply clarify
    1.23    apply (erule_tac P = "%x. x : S" in LeastI2)
    1.24     apply fast