equal
deleted
inserted
replaced
61 |
61 |
62 val quickcheck_generator = gen_quickcheck_generator (K I) (K I) |
62 val quickcheck_generator = gen_quickcheck_generator (K I) (K I) |
63 |
63 |
64 val quickcheck_generator_cmd = |
64 val quickcheck_generator_cmd = |
65 gen_quickcheck_generator |
65 gen_quickcheck_generator |
66 (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true}) |
66 ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true}) |
67 Syntax.read_term |
67 Syntax.read_term |
68 |
68 |
69 val _ = |
69 val _ = |
70 Outer_Syntax.command @{command_spec "quickcheck_generator"} |
70 Outer_Syntax.command @{command_spec "quickcheck_generator"} |
71 "define quickcheck generators for abstract types" |
71 "define quickcheck generators for abstract types" |