equal
deleted
inserted
replaced
34 * ML antiquotation @{code_datatype} inserts definition of a datatype |
34 * ML antiquotation @{code_datatype} inserts definition of a datatype |
35 generated by the code generator; see Predicate.thy for an example. |
35 generated by the code generator; see Predicate.thy for an example. |
36 |
36 |
37 * New method "linarith" invokes existing linear arithmetic decision |
37 * New method "linarith" invokes existing linear arithmetic decision |
38 procedure only. |
38 procedure only. |
|
39 |
|
40 * Implementation of quickcheck using generic code generator; default generators |
|
41 are provided for all suitable HOL types, records and datatypes. |
39 |
42 |
40 |
43 |
41 *** ML *** |
44 *** ML *** |
42 |
45 |
43 * Eliminated old Attrib.add_attributes, Method.add_methods and related |
46 * Eliminated old Attrib.add_attributes, Method.add_methods and related |