changeset 5143 | b94cd208f073 |
parent 5068 | fb28eaa07e01 |
child 5192 | 704dd3a6d47d |
--- a/src/HOLCF/Fix.ML Tue Jul 14 13:33:12 1998 +0200 +++ b/src/HOLCF/Fix.ML Wed Jul 15 10:15:13 1998 +0200 @@ -884,7 +884,7 @@ (Simp_tac 1) ]); -Goal "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \ +Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \ \ ==> adm (%x. P x = Q x)"; by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1); by (Asm_simp_tac 1);