# HG changeset patch
# User huffman
# Date 1112230369 -7200
# Node ID 99ed5113783b4a8d67c8a82b3f33a7dbe9924aab
# Parent  1fb24e545f88811b3c68ff3fc969ccbb3aef8511
cleaned up some proofs

diff -r 1fb24e545f88 -r 99ed5113783b src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Thu Mar 31 02:44:46 2005 +0200
+++ b/src/HOLCF/Discrete.thy	Thu Mar 31 02:52:49 2005 +0200
@@ -22,9 +22,7 @@
 less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
 
 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
-apply (unfold less_discr_def)
-apply (rule refl)
-done
+by (unfold less_discr_def) (rule refl)
 
 instance discr :: (type) po
 proof
@@ -46,17 +44,13 @@
 apply fast
 done
 
-lemma discr_chain_range0: 
+lemma discr_chain_range0 [simp]: 
  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
-apply (fast elim: discr_chain0)
-done
-declare discr_chain_range0 [simp]
+by (fast elim: discr_chain0)
 
 lemma discr_cpo: 
  "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
-apply (unfold is_lub_def is_ub_def)
-apply (simp (no_asm_simp))
-done
+by (unfold is_lub_def is_ub_def) simp
 
 instance discr :: (type) cpo
 by intro_classes (rule discr_cpo)