equal
deleted
inserted
replaced
15 in |
15 in |
16 InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st |
16 InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st |
17 end |
17 end |
18 *} |
18 *} |
19 |
19 |
|
20 ML {* |
|
21 fun mk_conjl props = |
|
22 fold (fn a => fn b => |
|
23 if a = @{term True} then b else |
|
24 if b = @{term True} then a else |
|
25 HOLogic.mk_conj (a, b)) (rev props) @{term True}; |
|
26 *} |
|
27 |
|
28 ML {* |
|
29 val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
|
30 *} |
20 |
31 |
21 |
32 |
22 ML {* |
33 ML {* |
23 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt = |
34 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt = |
24 let |
35 let |