equal
deleted
inserted
replaced
22 Library.funpow (length Ts) HOLogic.mk_split |
22 Library.funpow (length Ts) HOLogic.mk_split |
23 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
23 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
24 |
24 |
25 val split_all_tuples = |
25 val split_all_tuples = |
26 Simplifier.full_simplify (HOL_basic_ss addsimps |
26 Simplifier.full_simplify (HOL_basic_ss addsimps |
27 @{thms split_conv split_paired_all unit_all_eq1}) |
27 @{thms split_conv split_paired_all unit_all_eq1} @ |
28 (* |
28 @{thms fresh_Unit_elim fresh_Pair_elim} @ |
29 @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @ |
29 @{thms fresh_star_Unit_elim fresh_star_Pair_elim fresh_star_Un_elim} @ |
30 @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim}) |
30 @{thms fresh_star_insert_elim fresh_star_empty_elim}) |
31 *) |
|
32 |
31 |
33 |
32 |
34 (* prepare rule *) |
33 (* prepare rule *) |
35 |
34 |
36 fun inst_mutual_rule ctxt insts avoiding rules = |
35 fun inst_mutual_rule ctxt insts avoiding rules = |