changeset 51798 | ad3a241def73 |
parent 51717 | 9e7d1c139569 |
child 52241 | 5f6e885382e9 |
--- a/src/FOL/FOL.thy Sat Apr 27 11:37:50 2013 +0200 +++ b/src/FOL/FOL.thy Sat Apr 27 20:50:20 2013 +0200 @@ -150,7 +150,7 @@ proof (rule r) { fix y y' assume "P(y)" and "P(y')" - with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac 1")+ + with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+ then have "y = y'" by (rule subst) } note r' = this show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')