# HG changeset patch
# User huffman
# Date 1269318811 25200
# Node ID 85b0efdcdae9a2fc5c40f458367aa176ed6c56b0
# Parent  d5c5fc1b993b9c3320651f56880bf03bf1df6670
use fixrec_simp instead of fixpat

diff -r d5c5fc1b993b -r 85b0efdcdae9 src/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOLCF/ex/Powerdomain_ex.thy	Mon Mar 22 21:31:32 2010 -0700
+++ b/src/HOLCF/ex/Powerdomain_ex.thy	Mon Mar 22 21:33:31 2010 -0700
@@ -57,8 +57,8 @@
   mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a"
 | mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)"
 
-fixpat
-  mirror_strict [simp]: "mirror\<cdot>\<bottom>"
+lemma mirror_strict [simp]: "mirror\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
 
 fixrec
   pick :: "'a tree \<rightarrow> 'a convex_pd"
@@ -66,8 +66,8 @@
   pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
 | pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r"
 
-fixpat
-  pick_strict [simp]: "pick\<cdot>\<bottom>"
+lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
 
 lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t"
 by (induct t) (simp_all add: convex_plus_ac)