99 the local file system. |
99 the local file system. |
100 |
100 |
101 |
101 |
102 *** HOL *** |
102 *** HOL *** |
103 |
103 |
104 * Quickcheck now by default uses exhaustive testing instead of random testing. |
104 * Quickcheck now by default uses exhaustive testing instead of random |
105 Random testing can be invoked by quickcheck[random], |
105 testing. Random testing can be invoked by quickcheck[random], |
106 exhaustive testing by quickcheck[exhaustive]. |
106 exhaustive testing by quickcheck[exhaustive]. |
107 |
107 |
108 * Quickcheck instantiates polymorphic types with small finite datatypes |
108 * Quickcheck instantiates polymorphic types with small finite |
109 by default. This enables a simple execution mechanism to handle |
109 datatypes by default. This enables a simple execution mechanism to |
110 quantifiers and function equality over the finite datatypes. |
110 handle quantifiers and function equality over the finite datatypes. |
111 |
111 |
112 * Functions can be declared as coercions and type inference will add them |
112 * Functions can be declared as coercions and type inference will add |
113 as necessary upon input of a term. In Complex_Main, real :: nat => real |
113 them as necessary upon input of a term. In theory Complex_Main, |
114 and real :: int => real are declared as coercions. A new coercion function |
114 real :: nat => real and real :: int => real are declared as |
115 f is declared like this: |
115 coercions. A new coercion function f is declared like this: |
116 |
116 |
117 declare [[coercion f]] |
117 declare [[coercion f]] |
118 |
118 |
119 To lift coercions through type constructors (eg from nat => real to |
119 To lift coercions through type constructors (eg from nat => real to |
120 nat list => real list), map functions can be declared, e.g. |
120 nat list => real list), map functions can be declared, e.g. |
121 |
121 |
122 declare [[coercion_map map]] |
122 declare [[coercion_map map]] |
123 |
123 |
124 Currently coercion inference is activated only in theories including real |
124 Currently coercion inference is activated only in theories including |
125 numbers, i.e. descendants of Complex_Main. In other theories it needs to be |
125 real numbers, i.e. descendants of Complex_Main. This is controlled by |
126 loaded explicitly: uses "~~/src/Tools/subtyping.ML" |
126 the configuration option "infer_coercions", e.g. it can be enabled in |
|
127 other theories like this: |
|
128 |
|
129 declare [[coercion_enabled]] |
127 |
130 |
128 * Abandoned locales equiv, congruent and congruent2 for equivalence relations. |
131 * Abandoned locales equiv, congruent and congruent2 for equivalence relations. |
129 INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)). |
132 INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)). |
130 |
133 |
131 * Code generator: globbing constant expressions "*" and "Theory.*" have been |
134 * Code generator: globbing constant expressions "*" and "Theory.*" have been |