# HG changeset patch
# User huffman
# Date 1131402649 -3600
# Node ID 2b56f74fd6050c03b1cdff9f3a8e6bf9a017ca65
# Parent  08ec4f1f116dbe2930cb7703b730b16ad6e6326f
add case syntax for type one

diff -r 08ec4f1f116d -r 2b56f74fd605 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Mon Nov 07 19:23:53 2005 +0100
+++ b/src/HOLCF/One.thy	Mon Nov 07 23:30:49 2005 +0100
@@ -55,15 +55,16 @@
   "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)"
 
 translations
+  "case x of ONE \<Rightarrow> t" == "one_when\<cdot>t\<cdot>x"
   "\<Lambda> ONE. t" == "one_when\<cdot>t"
 
-lemma one_when1 [simp]: "(\<Lambda> ONE. t)\<cdot>\<bottom> = \<bottom>"
+lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
 by (simp add: one_when_def)
 
-lemma one_when2 [simp]: "(\<Lambda> ONE. t)\<cdot>ONE = t"
+lemma one_when2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
 by (simp add: one_when_def)
 
-lemma one_when3 [simp]: "(\<Lambda> ONE. ONE)\<cdot>x = x"
+lemma one_when3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
 by (rule_tac p=x in oneE, simp_all)
 
 end