# HG changeset patch
# User huffman
# Date 1120761672 -7200
# Node ID 934b6b36d794ae1e251ca12d6d3b74ecc9065e49
# Parent  3f3fbfd8ce041987f81390dd6758f736faad4295
cleaned up

diff -r 3f3fbfd8ce04 -r 934b6b36d794 src/HOLCF/One.thy
--- 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