equal
deleted
inserted
replaced
9 |
9 |
10 subsubsection "misc" |
10 subsubsection "misc" |
11 |
11 |
12 ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close> |
12 ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close> |
13 |
13 |
14 declare split_if_asm [split] option.split [split] option.split_asm [split] |
14 declare if_split_asm [split] option.split [split] option.split_asm [split] |
15 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close> |
15 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close> |
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] |
18 |
18 |
19 lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}" |
19 lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}" |