| changeset 1274 | ea0668a1c0ba |
| parent 1267 | bca91b4e1710 |
| child 1410 | 324aa8134639 |
--- a/src/HOLCF/Fix.ML Fri Oct 06 16:17:08 1995 +0100 +++ b/src/HOLCF/Fix.ML Fri Oct 06 17:25:24 1995 +0100 @@ -341,6 +341,19 @@ ]); +qed_goal "fix_eqI" Fix.thy +"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac antisym_less 1), + (etac allE 1), + (etac mp 1), + (rtac (fix_eq RS sym) 1), + (etac fix_least 1) + ]); + + qed_goal "fix_eq2" Fix.thy "f == fix`F ==> f = F`f" (fn prems => [