equal
deleted
inserted
replaced
82 |
82 |
83 |
83 |
84 *** Pure *** |
84 *** Pure *** |
85 |
85 |
86 * Command 'notepad' replaces former 'example_proof' for |
86 * Command 'notepad' replaces former 'example_proof' for |
87 experimentation in Isar without and result. INCOMPATIBILITY. |
87 experimentation in Isar without any result. INCOMPATIBILITY. |
88 |
88 |
89 * Support for real valued preferences (with approximative PGIP type). |
89 * Support for real valued preferences (with approximative PGIP type). |
90 |
90 |
91 * Interpretation command 'interpret' accepts a list of equations like |
91 * Interpretation command 'interpret' accepts a list of equations like |
92 'interpretation' does. |
92 'interpretation' does. |
131 |
131 |
132 declare [[coercion_map map]] |
132 declare [[coercion_map map]] |
133 |
133 |
134 Currently coercion inference is activated only in theories including |
134 Currently coercion inference is activated only in theories including |
135 real numbers, i.e. descendants of Complex_Main. This is controlled by |
135 real numbers, i.e. descendants of Complex_Main. This is controlled by |
136 the configuration option "infer_coercions", e.g. it can be enabled in |
136 the configuration option "coercion_enabled", e.g. it can be enabled in |
137 other theories like this: |
137 other theories like this: |
138 |
138 |
139 declare [[coercion_enabled]] |
139 declare [[coercion_enabled]] |
140 |
140 |
141 * Abandoned locales equiv, congruent and congruent2 for equivalence |
141 * Abandoned locales equiv, congruent and congruent2 for equivalence |