# HG changeset patch
# User huffman
# Date 1229626813 28800
# Node ID d5582ab1311f865561db3e43e80e438e13f6ab45
# Parent  6e0b7b11407268a032ebfb10d9eaca100dfc31f6
constdefs -> definition

diff -r 6e0b7b114072 -r d5582ab1311f src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Thu Dec 18 09:30:36 2008 -0800
+++ b/src/HOLCF/Fixrec.thy	Thu Dec 18 11:00:13 2008 -0800
@@ -16,13 +16,13 @@
 pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
 by simp_all
 
-constdefs
-  fail :: "'a maybe"
-  "fail \<equiv> Abs_maybe (sinl\<cdot>ONE)"
+definition
+  fail :: "'a maybe" where
+  "fail = Abs_maybe (sinl\<cdot>ONE)"
 
-constdefs
+definition
   return :: "'a \<rightarrow> 'a maybe" where
-  "return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))"
+  "return = (\<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x)))"
 
 definition
   maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" where
@@ -58,7 +58,8 @@
                   cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
 
 translations
-  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
+  "case m of XCONST fail \<Rightarrow> t1 | XCONST return\<cdot>x \<Rightarrow> t2"
+    == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
 
 
 subsubsection {* Monadic bind operator *}
@@ -163,8 +164,8 @@
 
 subsection {* Case branch combinator *}
 
-constdefs
-  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)"
+definition
+  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
   "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
 
 lemma branch_rews:
diff -r 6e0b7b114072 -r d5582ab1311f src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Thu Dec 18 09:30:36 2008 -0800
+++ b/src/HOLCF/One.thy	Thu Dec 18 11:00:13 2008 -0800
@@ -12,8 +12,9 @@
 translations
   "one" <= (type) "unit lift" 
 
-constdefs
+definition
   ONE :: "one"
+where
   "ONE == Def ()"
 
 text {* Exhaustion and Elimination for type @{typ one} *}