equal
deleted
inserted
replaced
204 (result, NONE) |
204 (result, NONE) |
205 end; |
205 end; |
206 |
206 |
207 |
207 |
208 val setup = |
208 val setup = |
209 Datatype.interpretation |
209 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
210 (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype)) |
210 (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype)) |
211 #> setup_finite_functions |
211 #> setup_finite_functions |
212 #> Context.theory_map |
212 #> Context.theory_map |
213 (Quickcheck.add_generator ("narrowing", compile_generator_expr)) |
213 (Quickcheck.add_generator ("narrowing", compile_generator_expr)) |
214 |
214 |
215 end; |
215 end; |