equal
deleted
inserted
replaced
9 |
9 |
10 ML {* |
10 ML {* |
11 Unify.search_bound := 40; |
11 Unify.search_bound := 40; |
12 Unify.trace_bound := 40; |
12 Unify.trace_bound := 40; |
13 *} |
13 *} |
14 (*print_depth 100;*) |
|
15 (*Syntax.ambiguity_level := 1;*) |
|
16 |
14 |
17 section "misc" |
15 section "misc" |
18 |
16 |
19 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
17 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
20 |
18 |
21 ML {* |
|
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)); |
|
24 *} |
|
25 |
|
26 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] |
27 ML {* |
20 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
28 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac)); |
|
29 *} |
|
30 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] |
31 declare length_Suc_conv [iff] |
22 declare length_Suc_conv [iff] |
32 |
23 |
33 (*###to be phased out *) |
24 (*###to be phased out *) |
34 ML {* |
25 ML {* |