equal
deleted
inserted
replaced
111 InductMethod.guess_instance |
111 InductMethod.guess_instance |
112 (finish_rule (InductMethod.internalize more_consumes rule)) i st' |
112 (finish_rule (InductMethod.internalize more_consumes rule)) i st' |
113 |> Seq.maps (fn rule' => |
113 |> Seq.maps (fn rule' => |
114 CASES (rule_cases rule' cases) |
114 CASES (rule_cases rule' cases) |
115 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
115 (Tactic.rtac (rename_params_rule false [] rule') i THEN |
116 PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st')))) |
116 PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) |
117 THEN_ALL_NEW_CASES InductMethod.rulify_tac |
117 THEN_ALL_NEW_CASES InductMethod.rulify_tac |
118 end; |
118 end; |
119 |
119 |
120 |
120 |
121 (* concrete syntax *) |
121 (* concrete syntax *) |