equal
deleted
inserted
replaced
206 *} |
206 *} |
207 |
207 |
208 datatype foo = Foo nat |
208 datatype foo = Foo nat |
209 |
209 |
210 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
210 local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] |
211 [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})] |
211 [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])] |
212 conf pat_completeness_auto #> snd*} |
212 conf pat_completeness_auto #> snd*} |
213 |
213 |
214 (*<*)end(*>*) |
214 (*<*)end(*>*) |