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