changeset 3836 | f1a1817659e6 |
parent 3511 | da4dd8b7ced4 |
child 3942 | 1f1c1f524d19 |
--- a/src/FOLP/ROOT.ML Fri Oct 10 15:52:12 1997 +0200 +++ b/src/FOLP/ROOT.ML Fri Oct 10 16:29:41 1997 +0200 @@ -33,7 +33,7 @@ (*etac rev_cut_eq moves an equality to be the last premise. *) val rev_cut_eq = prove_goal IFOLP.thy - "[| p:a=b; !!x.x:a=b ==> f(x):R |] ==> ?p:R" + "[| p:a=b; !!x. x:a=b ==> f(x):R |] ==> ?p:R" (fn prems => [ REPEAT(resolve_tac prems 1) ]); val rev_mp = rev_mp