equal
deleted
inserted
replaced
181 local val mktac = mk_case_split_inside_tac meta_iffD |
181 local val mktac = mk_case_split_inside_tac meta_iffD |
182 in |
182 in |
183 fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
183 fun split_inside_tac splits = mktac (map mk_meta_eq splits) |
184 end; |
184 end; |
185 |
185 |
|
186 val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos |
|
187 contrapos2 notnotD; |
186 |
188 |
187 (*** Standard simpsets ***) |
189 (*** Standard simpsets ***) |
188 |
190 |
189 structure Induction = InductionFun(struct val spec=IFOL.spec end); |
191 structure Induction = InductionFun(struct val spec=IFOL.spec end); |
190 |
192 |