equal
deleted
inserted
replaced
7 imports Main "~~/src/HOL/Library/Old_Recdef" |
7 imports Main "~~/src/HOL/Library/Old_Recdef" |
8 begin |
8 begin |
9 |
9 |
10 subsubsection "misc" |
10 subsubsection "misc" |
11 |
11 |
12 ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *} |
12 ML {* fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i) *} |
13 |
13 |
14 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] |
15 setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} |
15 setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} |
16 declare if_weak_cong [cong del] option.case_cong_weak [cong del] |
16 declare if_weak_cong [cong del] option.case_cong_weak [cong del] |
17 declare length_Suc_conv [iff] |
17 declare length_Suc_conv [iff] |