equal
deleted
inserted
replaced
17 section "misc" |
17 section "misc" |
18 |
18 |
19 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
19 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
20 |
20 |
21 ML {* |
21 ML {* |
22 fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat] |
22 fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat] |
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 {* |