equal
deleted
inserted
replaced
282 val allI = allI |
282 val allI = allI |
283 val allE = allE |
283 val allE = allE |
284 end); |
284 end); |
285 |
285 |
286 local |
286 local |
287 val ex_pattern = |
287 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
288 Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT) |
288 ("EX x. P(x) & Q(x)",HOLogic.boolT) |
289 |
289 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
290 val all_pattern = |
290 ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT) |
291 Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT) |
|
292 |
|
293 in |
291 in |
294 val defEX_regroup = |
292 val defEX_regroup = mk_simproc "defined EX" [ex_pattern] |
295 mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex; |
293 Quantifier1.rearrange_ex |
296 val defALL_regroup = |
294 val defALL_regroup = mk_simproc "defined ALL" [all_pattern] |
297 mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all; |
295 Quantifier1.rearrange_all |
298 end; |
296 end; |
299 |
297 |
300 |
298 |
301 (*** Case splitting ***) |
299 (*** Case splitting ***) |
302 |
300 |