equal
deleted
inserted
replaced
6 theory Basis |
6 theory Basis |
7 imports Main "~~/src/HOL/Library/Old_Recdef" |
7 imports Main "~~/src/HOL/Library/Old_Recdef" |
8 begin |
8 begin |
9 |
9 |
10 section "misc" |
10 section "misc" |
|
11 |
|
12 ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *} |
11 |
13 |
12 declare split_if_asm [split] option.split [split] option.split_asm [split] |
14 declare split_if_asm [split] option.split [split] option.split_asm [split] |
13 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
15 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
14 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
16 declare if_weak_cong [cong del] option.weak_case_cong [cong del] |
15 declare length_Suc_conv [iff] |
17 declare length_Suc_conv [iff] |