author | Christian Urban <urbanc@in.tum.de> |
Tue, 17 May 2011 19:46:53 +0200 | |
changeset 464 | 21b5d0145fe4 |
parent 463 | b6fc4d1b75d0 |
child 465 | 886a7c614ced |
ProgTutorial/Package/Ind_Extensions.thy | file | annotate | diff | comparison | revisions | |
progtutorial.pdf | file | annotate | diff | comparison | revisions |
--- a/ProgTutorial/Package/Ind_Extensions.thy Tue May 17 19:25:33 2011 +0200 +++ b/ProgTutorial/Package/Ind_Extensions.thy Tue May 17 19:46:53 2011 +0200 @@ -197,7 +197,7 @@ ML{*fun pat_completeness_auto ctxt = Pat_Completeness.pat_completeness_tac ctxt 1 - THEN auto_tac (clasimpset_of ctxt)*} + THEN auto_tac ctxt*} ML {* val conf = Function_Common.default_config