src/HOLCF/Fixrec.thy
changeset 33429 42d7b6b4992b
parent 33425 7e4f3c66190d
child 35115 446c5063e4fd
     1.1 --- a/src/HOLCF/Fixrec.thy	Tue Nov 03 18:32:56 2009 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Tue Nov 03 18:33:16 2009 -0800
     1.3 @@ -622,6 +622,7 @@
     1.4  
     1.5  lemmas [fixrec_simp] =
     1.6    run_strict run_fail run_return
     1.7 +  mplus_strict mplus_fail mplus_return
     1.8    spair_strict_iff
     1.9    sinl_defined_iff
    1.10    sinr_defined_iff