equal
deleted
inserted
replaced
122 local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) |
122 local val mktac = mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) |
123 in |
123 in |
124 fun split_tac splits = mktac (map mk_meta_eq splits) |
124 fun split_tac splits = mktac (map mk_meta_eq splits) |
125 end; |
125 end; |
126 |
126 |
|
127 local val mktac = mk_case_split_inside_tac (meta_eq_to_obj_eq RS iffD2) |
|
128 in |
|
129 fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
|
130 end; |
|
131 |
127 |
132 |
128 (* eliminiation of existential quantifiers in assumptions *) |
133 (* eliminiation of existential quantifiers in assumptions *) |
129 |
134 |
130 val ex_all_equiv = |
135 val ex_all_equiv = |
131 let val lemma1 = prove_goal HOL.thy |
136 let val lemma1 = prove_goal HOL.thy |