equal
deleted
inserted
replaced
193 text {* Type declarations *} |
193 text {* Type declarations *} |
194 |
194 |
195 ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn) |
195 ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn) |
196 @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} |
196 @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} |
197 |
197 |
|
198 ML{*fun pat_completeness_auto ctxt = |
|
199 Pat_Completeness.pat_completeness_tac ctxt 1 |
|
200 THEN auto_tac (clasimpset_of ctxt)*} |
|
201 |
|
202 ML {* |
|
203 val conf = Function_Common.default_config |
|
204 *} |
|
205 |
|
206 datatype foo = Foo nat |
|
207 |
|
208 local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] |
|
209 [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})] |
|
210 #> snd *} |
|
211 |
|
212 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
|
213 [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})] |
|
214 conf pat_completeness_auto #> snd*} |
198 |
215 |
199 (*<*)end(*>*) |
216 (*<*)end(*>*) |