changeset 464 | 21b5d0145fe4 |
parent 423 | 0a25b35178c3 |
child 517 | d8c376662bb4 |
--- 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