equal
deleted
inserted
replaced
18 |
18 |
19 declare split_if_asm [split] option.split [split] option.split_asm [split] |
19 declare split_if_asm [split] option.split [split] option.split_asm [split] |
20 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
20 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
21 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
21 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
22 declare length_Suc_conv [iff] |
22 declare length_Suc_conv [iff] |
23 |
|
24 (*###to be phased out *) |
|
25 ML {* |
|
26 bind_thm ("make_imp", rearrange_prems [1,0] mp) |
|
27 *} |
|
28 |
23 |
29 lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}" |
24 lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}" |
30 apply auto |
25 apply auto |
31 done |
26 done |
32 |
27 |