equal
deleted
inserted
replaced
5 |
5 |
6 theory Basis imports Main begin |
6 theory Basis imports Main begin |
7 |
7 |
8 |
8 |
9 section "misc" |
9 section "misc" |
10 |
|
11 declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) |
|
12 |
10 |
13 declare split_if_asm [split] option.split [split] option.split_asm [split] |
11 declare split_if_asm [split] option.split [split] option.split_asm [split] |
14 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
12 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
15 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
13 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
16 declare length_Suc_conv [iff] |
14 declare length_Suc_conv [iff] |