--- a/src/HOLCF/Fixrec.thy Mon Nov 02 18:49:53 2009 -0800
+++ b/src/HOLCF/Fixrec.thy Tue Nov 03 17:03:21 2009 -0800
@@ -620,4 +620,22 @@
hide (open) const return bind fail run cases
+lemmas [fixrec_simp] =
+ run_strict run_fail run_return
+ spair_strict_iff
+ sinl_defined_iff
+ sinr_defined_iff
+ up_defined
+ ONE_defined
+ dist_eq_tr(1,2)
+ match_UU_simps
+ match_cpair_simps
+ match_spair_simps
+ match_sinl_simps
+ match_sinr_simps
+ match_up_simps
+ match_ONE_simps
+ match_TT_simps
+ match_FF_simps
+
end