changeset 2688 | 889a1cbd1aca |
parent 2414 | 13df7d6c5c3b |
child 3925 | 90f499226ab9 |
--- a/src/ZF/intr_elim.ML Fri Feb 28 15:44:32 1997 +0100 +++ b/src/ZF/intr_elim.ML Fri Feb 28 15:46:41 1997 +0100 @@ -155,7 +155,8 @@ rule_by_tactic (rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs) - (assume_read Inductive.thy s RS elim); + (assume_read Inductive.thy s RS elim) + |> standard; val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) and rec_names = rec_names