equal
deleted
inserted
replaced
205 val conf = Function_Common.default_config |
205 val conf = Function_Common.default_config |
206 *} |
206 *} |
207 |
207 |
208 datatype foo = Foo nat |
208 datatype foo = Foo nat |
209 |
209 |
210 local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] |
|
211 [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})] |
|
212 #> snd *} |
|
213 |
|
214 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
210 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
215 [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})] |
211 [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})] |
216 conf pat_completeness_auto #> snd*} |
212 conf pat_completeness_auto #> snd*} |
217 |
213 |
218 (*<*)end(*>*) |
214 (*<*)end(*>*) |