src/HOL/Typedef.thy
changeset 11982 65e2822d83dd
parent 11979 0a3dace545c5
child 12023 d982f98e0f0d
     1.1 --- a/src/HOL/Typedef.thy	Mon Oct 29 17:22:18 2001 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Tue Oct 30 13:43:26 2001 +0100
     1.3 @@ -8,18 +8,6 @@
     1.4  theory Typedef = Set
     1.5  files ("Tools/typedef_package.ML"):
     1.6  
     1.7 -lemma Least_mono: 
     1.8 -  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
     1.9 -    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    1.10 -    -- {* Courtesy of Stephan Merz *}
    1.11 -  apply clarify
    1.12 -  apply (erule_tac P = "%x. x : S" in LeastI2)
    1.13 -   apply fast
    1.14 -  apply (rule LeastI2)
    1.15 -  apply (auto elim: monoD intro!: order_antisym)
    1.16 -  done
    1.17 -
    1.18 -
    1.19  subsection {* HOL type definitions *}
    1.20  
    1.21  constdefs