--- a/src/HOLCF/One.thy Thu Jul 07 19:55:46 2005 +0200
+++ b/src/HOLCF/One.thy Thu Jul 07 20:41:12 2005 +0200
@@ -15,36 +15,34 @@
constdefs
ONE :: "one"
- "ONE == Def ()"
+ "ONE \<equiv> Def ()"
translations
"one" <= (type) "unit lift"
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion and Elimination for type one *)
-(* ------------------------------------------------------------------------ *)
+text {* Exhaustion and Elimination for type @{typ one} *}
-lemma Exh_one: "t=UU | t = ONE"
+lemma Exh_one: "t = \<bottom> \<or> t = ONE"
apply (unfold ONE_def)
apply (induct t)
apply simp
apply simp
done
-lemma oneE: "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"
+lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
apply (rule Exh_one [THEN disjE])
apply fast
apply fast
done
-lemma dist_less_one [simp]: "~ONE << UU"
+lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
apply (unfold ONE_def)
-apply (simp add: inst_lift_po)
+apply simp
done
-lemma dist_eq_one [simp]: "ONE~=UU" "UU~=ONE"
+lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
apply (unfold ONE_def)
-apply (simp_all add: inst_lift_po)
+apply simp_all
done
end