diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/Package/Ind_Extensions.thy --- a/ProgTutorial/Package/Ind_Extensions.thy Mon Apr 26 05:20:01 2010 +0200 +++ b/ProgTutorial/Package/Ind_Extensions.thy Mon May 17 17:27:21 2010 +0100 @@ -195,5 +195,22 @@ ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn) @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} +ML{*fun pat_completeness_auto ctxt = + Pat_Completeness.pat_completeness_tac ctxt 1 + THEN auto_tac (clasimpset_of ctxt)*} + +ML {* + val conf = Function_Common.default_config +*} + +datatype foo = Foo nat + +local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] + [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})] + #> snd *} + +local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] + [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})] + conf pat_completeness_auto #> snd*} (*<*)end(*>*) \ No newline at end of file