equal
deleted
inserted
replaced
372 *} |
372 *} |
373 |
373 |
374 method_setup possibility = {* |
374 method_setup possibility = {* |
375 Method.ctxt_args (fn ctxt => |
375 Method.ctxt_args (fn ctxt => |
376 Method.METHOD (fn facts => |
376 Method.METHOD (fn facts => |
377 gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
377 gen_possibility_tac (local_simpset_of ctxt))) *} |
378 "for proving possibility theorems" |
378 "for proving possibility theorems" |
379 |
379 |
380 |
380 |
381 |
381 |
382 subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} |
382 subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} |