equal
deleted
inserted
replaced
23 (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm)); |
23 (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm)); |
24 *} |
24 *} |
25 |
25 |
26 declare split_if_asm [split] option.split [split] option.split_asm [split] |
26 declare split_if_asm [split] option.split [split] option.split_asm [split] |
27 ML {* |
27 ML {* |
28 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
28 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac)); |
29 *} |
29 *} |
30 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
30 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
31 declare length_Suc_conv [iff]; |
31 declare length_Suc_conv [iff]; |
32 |
32 |
33 (*###to be phased out *) |
33 (*###to be phased out *) |