diff -r 9d4d70b175fd -r c1a7490ee3ff src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Thu Nov 03 01:28:22 2005 +0100
+++ b/src/HOLCF/One.thy	Thu Nov 03 01:44:27 2005 +0100
@@ -48,4 +48,22 @@
 lemma compact_ONE [simp]: "compact ONE"
 by (rule compact_chfin)
 
+text {* Case analysis function for type @{typ one} *}
+
+constdefs
+  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
+  "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)"
+
+translations
+  "\<Lambda> ONE. t" == "one_when\<cdot>t"
+
+lemma one_when1 [simp]: "(\<Lambda> ONE. t)\<cdot>\<bottom> = \<bottom>"
+by (simp add: one_when_def)
+
+lemma one_when2 [simp]: "(\<Lambda> ONE. t)\<cdot>ONE = t"
+by (simp add: one_when_def)
+
+lemma one_when3 [simp]: "(\<Lambda> ONE. ONE)\<cdot>x = x"
+by (rule_tac p=x in oneE, simp_all)
+
 end