# HG changeset patch
# User huffman
# Date 1257301996 28800
# Node ID 42d7b6b4992ba291f10a3ccf41621e74171feee1
# Parent  70ed971a79d1f4a569787978e041a2b06d0717a5
add more fixrec_simp rules

diff -r 70ed971a79d1 -r 42d7b6b4992b src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Tue Nov 03 18:32:56 2009 -0800
+++ b/src/HOLCF/Fixrec.thy	Tue Nov 03 18:33:16 2009 -0800
@@ -622,6 +622,7 @@
 
 lemmas [fixrec_simp] =
   run_strict run_fail run_return
+  mplus_strict mplus_fail mplus_return
   spair_strict_iff
   sinl_defined_iff
   sinr_defined_iff