| changeset 27208 | 5fe899199f85 |
| parent 19755 | 90f80de04c46 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/LCF/ex/Ex4.thy Sat Jun 14 17:49:24 2008 +0200 +++ b/src/LCF/ex/Ex4.thy Sat Jun 14 23:19:51 2008 +0200 @@ -10,7 +10,7 @@ shows "FIX(f)=p" apply (unfold eq_def) apply (rule conjI) - apply (tactic {* induct_tac "f" 1 *}) + apply (tactic {* induct_tac @{context} "f" 1 *}) apply (rule minimal) apply (intro strip) apply (rule less_trans)