equal
deleted
inserted
replaced
63 |
63 |
64 (* @chunk induction_tac *) |
64 (* @chunk induction_tac *) |
65 fun induction_tac defs prems insts = |
65 fun induction_tac defs prems insts = |
66 EVERY1 [ObjectLogic.full_atomize_tac, |
66 EVERY1 [ObjectLogic.full_atomize_tac, |
67 cut_facts_tac prems, |
67 cut_facts_tac prems, |
68 K (rewrite_goals_tac defs), |
68 rewrite_goal_tac defs, |
69 EVERY' (map (dtac o inst_spec) insts), |
69 EVERY' (map (dtac o inst_spec) insts), |
70 assume_tac] |
70 assume_tac] |
71 (* @end *) |
71 (* @end *) |
72 |
72 |
73 (* @chunk induction_rules *) |
73 (* @chunk induction_rules *) |
137 end) |
137 end) |
138 (* @end *) |
138 (* @end *) |
139 |
139 |
140 fun introductions_tac defs rules preds i ctxt = |
140 fun introductions_tac defs rules preds i ctxt = |
141 EVERY1 [ObjectLogic.rulify_tac, |
141 EVERY1 [ObjectLogic.rulify_tac, |
142 K (rewrite_goals_tac defs), |
142 rewrite_goal_tac defs, |
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
144 subproof1 rules preds i ctxt] |
144 subproof1 rules preds i ctxt] |
145 |
145 |
146 |
146 |
147 (* @chunk intro_rules *) |
147 (* @chunk intro_rules *) |