src/HOLCF/Discrete.thy
changeset 15639 99ed5113783b
parent 15590 17f4f5afcd5f
child 16070 4a83dd540b88
     1.1 --- a/src/HOLCF/Discrete.thy	Thu Mar 31 02:44:46 2005 +0200
     1.2 +++ b/src/HOLCF/Discrete.thy	Thu Mar 31 02:52:49 2005 +0200
     1.3 @@ -22,9 +22,7 @@
     1.4  less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
     1.5  
     1.6  lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
     1.7 -apply (unfold less_discr_def)
     1.8 -apply (rule refl)
     1.9 -done
    1.10 +by (unfold less_discr_def) (rule refl)
    1.11  
    1.12  instance discr :: (type) po
    1.13  proof
    1.14 @@ -46,17 +44,13 @@
    1.15  apply fast
    1.16  done
    1.17  
    1.18 -lemma discr_chain_range0: 
    1.19 +lemma discr_chain_range0 [simp]: 
    1.20   "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
    1.21 -apply (fast elim: discr_chain0)
    1.22 -done
    1.23 -declare discr_chain_range0 [simp]
    1.24 +by (fast elim: discr_chain0)
    1.25  
    1.26  lemma discr_cpo: 
    1.27   "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
    1.28 -apply (unfold is_lub_def is_ub_def)
    1.29 -apply (simp (no_asm_simp))
    1.30 -done
    1.31 +by (unfold is_lub_def is_ub_def) simp
    1.32  
    1.33  instance discr :: (type) cpo
    1.34  by intro_classes (rule discr_cpo)