src/HOLCF/Discrete.thy

--- a/src/HOLCF/Discrete.thy	Tue Mar 08 00:11:49 2005 +0100
+++ b/src/HOLCF/Discrete.thy	Tue Mar 08 00:15:01 2005 +0100
@@ -14,6 +14,8 @@
 
 datatype 'a discr = Discr "'a :: type"
 
+subsection {* Type @{typ "'a discr"} is a partial order *}
+
 instance discr :: (type) sq_ord ..
 
 defs (overloaded)
@@ -32,6 +34,8 @@
   { assume "x << y" and "y << z" thus "x << z" by simp }
 qed
 
+subsection {* Type @{typ "'a discr"} is a cpo *}
+
 lemma discr_chain0: 
  "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
 apply (unfold chain_def)
@@ -54,26 +58,25 @@
 apply (simp (no_asm_simp))
 done
 
-instance discr :: (type)cpo
-by (intro_classes, rule discr_cpo)
+instance discr :: (type) cpo
+by intro_classes (rule discr_cpo)
+
+subsection {* @{term undiscr} *}
 
 constdefs
    undiscr :: "('a::type)discr => 'a"
   "undiscr x == (case x of Discr y => y)"
 
 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
-apply (unfold undiscr_def)
-apply (simp (no_asm))
-done
+by (simp add: undiscr_def)
 
 lemma discr_chain_f_range0:
  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
-apply (fast dest: discr_chain0 elim: arg_cong)
-done
+by (fast dest: discr_chain0 elim: arg_cong)
 
 lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
 apply (unfold cont is_lub_def is_ub_def)
-apply (simp (no_asm) add: discr_chain_f_range0)
+apply (simp add: discr_chain_f_range0)
 done
 
 end