equal
deleted
inserted
replaced
17 |
17 |
18 section "misc" |
18 section "misc" |
19 |
19 |
20 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
20 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
21 |
21 |
22 (* ###TO HOL/???.ML?? *) |
|
23 ML {* |
22 ML {* |
24 fun make_simproc name pat pred thm = Simplifier.mk_simproc name |
23 fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat] |
25 [Thm.read_cterm (Thm.sign_of_thm thm) (pat, HOLogic.typeT)] |
24 (fn _ => fn _ => fn t => if pred t then None else Some (mk_meta_eq thm)); |
26 (K (K (fn s => if pred s then None else Some (standard (mk_meta_eq thm))))) |
|
27 *} |
25 *} |
28 |
26 |
29 declare split_if_asm [split] option.split [split] option.split_asm [split] |
27 declare split_if_asm [split] option.split [split] option.split_asm [split] |
30 ML {* |
28 ML {* |
31 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
29 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |