equal
deleted
inserted
replaced
24 |
24 |
25 * ML antiquotation @{code_datatype} inserts definition of a datatype generated |
25 * ML antiquotation @{code_datatype} inserts definition of a datatype generated |
26 by the code generator; see Predicate.thy for an example. |
26 by the code generator; see Predicate.thy for an example. |
27 |
27 |
28 * New method "linarith" invokes existing linear arithmetic decision procedure only. |
28 * New method "linarith" invokes existing linear arithmetic decision procedure only. |
|
29 |
|
30 * Implementation of quickcheck using generic code generator; default generators |
|
31 are provided for all suitable HOL types, records and datatypes. |
29 |
32 |
30 |
33 |
31 *** ML *** |
34 *** ML *** |
32 |
35 |
33 * Eliminated old Attrib.add_attributes, Method.add_methods and related |
36 * Eliminated old Attrib.add_attributes, Method.add_methods and related |