143 locale fun_left_comm_idem ~> locale comp_fun_idem |
130 locale fun_left_comm_idem ~> locale comp_fun_idem |
144 |
131 |
145 Both use point-free characterization; interpretation proofs may need |
132 Both use point-free characterization; interpretation proofs may need |
146 adjustment. INCOMPATIBILITY. |
133 adjustment. INCOMPATIBILITY. |
147 |
134 |
148 * Code generation: |
|
149 |
|
150 - Theory Library/Code_Char_ord provides native ordering of |
|
151 characters in the target language. |
|
152 |
|
153 - Commands code_module and code_library are legacy, use export_code |
|
154 instead. |
|
155 |
|
156 - Method "evaluation" is legacy, use method "eval" instead. |
|
157 |
|
158 - Legacy evaluator "SML" is deactivated by default. May be |
|
159 reactivated by the following theory command: |
|
160 |
|
161 setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} |
|
162 |
|
163 * Declare ext [intro] by default. Rare INCOMPATIBILITY. |
|
164 |
|
165 * Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is |
|
166 still available as a legacy feature for some time. |
|
167 |
|
168 * Nitpick: |
|
169 - Added "need" and "total_consts" options. |
|
170 - Reintroduced "show_skolems" option by popular demand. |
|
171 - Renamed attribute: nitpick_def ~> nitpick_unfold. |
|
172 INCOMPATIBILITY. |
|
173 |
|
174 * Sledgehammer: |
|
175 - Use quasi-sound (and efficient) translations by default. |
|
176 - Added support for the following provers: E-ToFoF, LEO-II, |
|
177 Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. |
|
178 - Automatically preplay and minimize proofs before showing them if |
|
179 this can be done within reasonable time. |
|
180 - sledgehammer available_provers ~> sledgehammer supported_provers. |
|
181 INCOMPATIBILITY. |
|
182 - Added "preplay_timeout", "slicing", "type_enc", "sound", |
|
183 "max_mono_iters", and "max_new_mono_instances" options. |
|
184 - Removed "explicit_apply" and "full_types" options as well as "Full |
|
185 Types" Proof General menu item. INCOMPATIBILITY. |
|
186 |
|
187 * Metis: |
|
188 - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. |
|
189 - Obsoleted "metisFT" -- use "metis (full_types)" instead. |
|
190 INCOMPATIBILITY. |
|
191 |
|
192 * Command 'try': |
|
193 - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and |
|
194 "elim:" options. INCOMPATIBILITY. |
|
195 - Introduced 'try' that not only runs 'try_methods' but also |
|
196 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. |
|
197 |
|
198 * Quickcheck: |
|
199 - Added "eval" option to evaluate terms for the found counterexample |
|
200 (currently only supported by the default (exhaustive) tester). |
|
201 - Added post-processing of terms to obtain readable counterexamples |
|
202 (currently only supported by the default (exhaustive) tester). |
|
203 - New counterexample generator quickcheck[narrowing] enables |
|
204 narrowing-based testing. Requires the Glasgow Haskell compiler |
|
205 with its installation location defined in the Isabelle settings |
|
206 environment as ISABELLE_GHC. |
|
207 - Removed quickcheck tester "SML" based on the SML code generator |
|
208 (formly in HOL/Library). |
|
209 |
|
210 * Function package: discontinued option "tailrec". INCOMPATIBILITY, |
|
211 use 'partial_function' instead. |
|
212 |
|
213 * Session HOL-Probability: |
|
214 - Caratheodory's extension lemma is now proved for ring_of_sets. |
|
215 - Infinite products of probability measures are now available. |
|
216 - Sigma closure is independent, if the generator is independent |
|
217 - Use extended reals instead of positive extended |
|
218 reals. INCOMPATIBILITY. |
|
219 |
|
220 * Theory Library/Extended_Reals replaces now the positive extended |
|
221 reals found in probability theory. This file is extended by |
|
222 Multivariate_Analysis/Extended_Real_Limits. |
|
223 |
|
224 * Old 'recdef' package has been moved to theory Library/Old_Recdef, |
|
225 from where it must be imported explicitly. INCOMPATIBILITY. |
|
226 |
|
227 * Well-founded recursion combinator "wfrec" has been moved to theory |
|
228 Library/Wfrec. INCOMPATIBILITY. |
|
229 |
|
230 * Theory HOL/Library/Cset_Monad allows do notation for computable sets |
|
231 (cset) via the generic monad ad-hoc overloading facility. |
|
232 |
|
233 * Theories of common data structures are split into theories for |
|
234 implementation, an invariant-ensuring type, and connection to an |
|
235 abstract type. INCOMPATIBILITY. |
|
236 |
|
237 - RBT is split into RBT and RBT_Mapping. |
|
238 - AssocList is split and renamed into AList and AList_Mapping. |
|
239 - DList is split into DList_Impl, DList, and DList_Cset. |
|
240 - Cset is split into Cset and List_Cset. |
|
241 |
|
242 * Theory Library/Nat_Infinity has been renamed to |
|
243 Library/Extended_Nat, with name changes of the following types and |
|
244 constants: |
|
245 |
|
246 type inat ~> type enat |
|
247 Fin ~> enat |
|
248 Infty ~> infinity (overloaded) |
|
249 iSuc ~> eSuc |
|
250 the_Fin ~> the_enat |
|
251 |
|
252 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has |
|
253 been renamed accordingly. INCOMPATIBILITY. |
|
254 |
|
255 * Theory Limits: Type "'a net" has been renamed to "'a filter", in |
135 * Theory Limits: Type "'a net" has been renamed to "'a filter", in |
256 accordance with standard mathematical terminology. INCOMPATIBILITY. |
136 accordance with standard mathematical terminology. INCOMPATIBILITY. |
257 |
|
258 * Session Multivariate_Analysis: The euclidean_space type class now |
|
259 fixes a constant "Basis :: 'a set" consisting of the standard |
|
260 orthonormal basis for the type. Users now have the option of |
|
261 quantifying over this set instead of using the "basis" function, e.g. |
|
262 "ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)". |
|
263 |
|
264 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed |
|
265 to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants |
|
266 "Cart_nth" and "Cart_lambda" have been respectively renamed to |
|
267 "vec_nth" and "vec_lambda"; theorems mentioning those names have |
|
268 changed to match. Definition theorems for overloaded constants now use |
|
269 the standard "foo_vec_def" naming scheme. A few other theorems have |
|
270 been renamed as follows (INCOMPATIBILITY): |
|
271 |
|
272 Cart_eq ~> vec_eq_iff |
|
273 dist_nth_le_cart ~> dist_vec_nth_le |
|
274 tendsto_vector ~> vec_tendstoI |
|
275 Cauchy_vector ~> vec_CauchyI |
|
276 |
|
277 * Session Multivariate_Analysis: Several duplicate theorems have been |
|
278 removed, and other theorems have been renamed or replaced with more |
|
279 general versions. INCOMPATIBILITY. |
|
280 |
|
281 finite_choice ~> finite_set_choice |
|
282 eventually_conjI ~> eventually_conj |
|
283 eventually_and ~> eventually_conj_iff |
|
284 eventually_false ~> eventually_False |
|
285 setsum_norm ~> norm_setsum |
|
286 Lim_sequentially ~> LIMSEQ_def |
|
287 Lim_ident_at ~> LIM_ident |
|
288 Lim_const ~> tendsto_const |
|
289 Lim_cmul ~> tendsto_scaleR [OF tendsto_const] |
|
290 Lim_neg ~> tendsto_minus |
|
291 Lim_add ~> tendsto_add |
|
292 Lim_sub ~> tendsto_diff |
|
293 Lim_mul ~> tendsto_scaleR |
|
294 Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] |
|
295 Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] |
|
296 Lim_linear ~> bounded_linear.tendsto |
|
297 Lim_component ~> tendsto_euclidean_component |
|
298 Lim_component_cart ~> tendsto_vec_nth |
|
299 Lim_inner ~> tendsto_inner [OF tendsto_const] |
|
300 dot_lsum ~> inner_setsum_left |
|
301 dot_rsum ~> inner_setsum_right |
|
302 continuous_cmul ~> continuous_scaleR [OF continuous_const] |
|
303 continuous_neg ~> continuous_minus |
|
304 continuous_sub ~> continuous_diff |
|
305 continuous_vmul ~> continuous_scaleR [OF _ continuous_const] |
|
306 continuous_mul ~> continuous_scaleR |
|
307 continuous_inv ~> continuous_inverse |
|
308 continuous_at_within_inv ~> continuous_at_within_inverse |
|
309 continuous_at_inv ~> continuous_at_inverse |
|
310 continuous_at_norm ~> continuous_norm [OF continuous_at_id] |
|
311 continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] |
|
312 continuous_at_component ~> continuous_component [OF continuous_at_id] |
|
313 continuous_on_neg ~> continuous_on_minus |
|
314 continuous_on_sub ~> continuous_on_diff |
|
315 continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] |
|
316 continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] |
|
317 continuous_on_mul ~> continuous_on_scaleR |
|
318 continuous_on_mul_real ~> continuous_on_mult |
|
319 continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] |
|
320 continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] |
|
321 continuous_on_inverse ~> continuous_on_inv |
|
322 uniformly_continuous_on_neg ~> uniformly_continuous_on_minus |
|
323 uniformly_continuous_on_sub ~> uniformly_continuous_on_diff |
|
324 subset_interior ~> interior_mono |
|
325 subset_closure ~> closure_mono |
|
326 closure_univ ~> closure_UNIV |
|
327 real_arch_lt ~> reals_Archimedean2 |
|
328 real_arch ~> reals_Archimedean3 |
|
329 real_abs_norm ~> abs_norm_cancel |
|
330 real_abs_sub_norm ~> norm_triangle_ineq3 |
|
331 norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 |
|
332 |
137 |
333 * Theory Complex_Main: The locale interpretations for the |
138 * Theory Complex_Main: The locale interpretations for the |
334 bounded_linear and bounded_bilinear locales have been removed, in |
139 bounded_linear and bounded_bilinear locales have been removed, in |
335 order to reduce the number of duplicate lemmas. Users must use the |
140 order to reduce the number of duplicate lemmas. Users must use the |
336 original names for distributivity theorems, potential INCOMPATIBILITY. |
141 original names for distributivity theorems, potential INCOMPATIBILITY. |
415 |
220 |
416 * Theory Complex_Main: The complex exponential function "expi" is now |
221 * Theory Complex_Main: The complex exponential function "expi" is now |
417 a type-constrained abbreviation for "exp :: complex => complex"; thus |
222 a type-constrained abbreviation for "exp :: complex => complex"; thus |
418 several polymorphic lemmas about "exp" are now applicable to "expi". |
223 several polymorphic lemmas about "exp" are now applicable to "expi". |
419 |
224 |
|
225 * Code generation: |
|
226 |
|
227 - Theory Library/Code_Char_ord provides native ordering of |
|
228 characters in the target language. |
|
229 |
|
230 - Commands code_module and code_library are legacy, use export_code |
|
231 instead. |
|
232 |
|
233 - Method "evaluation" is legacy, use method "eval" instead. |
|
234 |
|
235 - Legacy evaluator "SML" is deactivated by default. May be |
|
236 reactivated by the following theory command: |
|
237 |
|
238 setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} |
|
239 |
|
240 * Declare ext [intro] by default. Rare INCOMPATIBILITY. |
|
241 |
|
242 * Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is |
|
243 still available as a legacy feature for some time. |
|
244 |
|
245 * Nitpick: |
|
246 - Added "need" and "total_consts" options. |
|
247 - Reintroduced "show_skolems" option by popular demand. |
|
248 - Renamed attribute: nitpick_def ~> nitpick_unfold. |
|
249 INCOMPATIBILITY. |
|
250 |
|
251 * Sledgehammer: |
|
252 - Use quasi-sound (and efficient) translations by default. |
|
253 - Added support for the following provers: E-ToFoF, LEO-II, |
|
254 Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. |
|
255 - Automatically preplay and minimize proofs before showing them if |
|
256 this can be done within reasonable time. |
|
257 - sledgehammer available_provers ~> sledgehammer supported_provers. |
|
258 INCOMPATIBILITY. |
|
259 - Added "preplay_timeout", "slicing", "type_enc", "sound", |
|
260 "max_mono_iters", and "max_new_mono_instances" options. |
|
261 - Removed "explicit_apply" and "full_types" options as well as "Full |
|
262 Types" Proof General menu item. INCOMPATIBILITY. |
|
263 |
|
264 * Metis: |
|
265 - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. |
|
266 - Obsoleted "metisFT" -- use "metis (full_types)" instead. |
|
267 INCOMPATIBILITY. |
|
268 |
|
269 * Command 'try': |
|
270 - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and |
|
271 "elim:" options. INCOMPATIBILITY. |
|
272 - Introduced 'try' that not only runs 'try_methods' but also |
|
273 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. |
|
274 |
|
275 * Quickcheck: |
|
276 - Added "eval" option to evaluate terms for the found counterexample |
|
277 (currently only supported by the default (exhaustive) tester). |
|
278 - Added post-processing of terms to obtain readable counterexamples |
|
279 (currently only supported by the default (exhaustive) tester). |
|
280 - New counterexample generator quickcheck[narrowing] enables |
|
281 narrowing-based testing. Requires the Glasgow Haskell compiler |
|
282 with its installation location defined in the Isabelle settings |
|
283 environment as ISABELLE_GHC. |
|
284 - Removed quickcheck tester "SML" based on the SML code generator |
|
285 (formly in HOL/Library). |
|
286 |
|
287 * Function package: discontinued option "tailrec". INCOMPATIBILITY, |
|
288 use 'partial_function' instead. |
|
289 |
|
290 * Theory Library/Extended_Reals replaces now the positive extended |
|
291 reals found in probability theory. This file is extended by |
|
292 Multivariate_Analysis/Extended_Real_Limits. |
|
293 |
|
294 * Old 'recdef' package has been moved to theory Library/Old_Recdef, |
|
295 from where it must be imported explicitly. INCOMPATIBILITY. |
|
296 |
|
297 * Theory Library/Wfrec: well-founded recursion combinator "wfrec" has |
|
298 been moved here. INCOMPATIBILITY. |
|
299 |
|
300 * Theory Library/Saturated provides type of numbers with saturated |
|
301 arithmetic. |
|
302 |
|
303 * Theory Library/Product_Lattice defines a pointwise ordering for the |
|
304 product type 'a * 'b, and provides instance proofs for various order |
|
305 and lattice type classes. |
|
306 |
|
307 * Theory Library/Countable now provides the "countable_datatype" proof |
|
308 method for proving "countable" class instances for datatypes. |
|
309 |
|
310 * Theory Library/Cset_Monad allows do notation for computable sets |
|
311 (cset) via the generic monad ad-hoc overloading facility. |
|
312 |
|
313 * Library: Theories of common data structures are split into theories |
|
314 for implementation, an invariant-ensuring type, and connection to an |
|
315 abstract type. INCOMPATIBILITY. |
|
316 |
|
317 - RBT is split into RBT and RBT_Mapping. |
|
318 - AssocList is split and renamed into AList and AList_Mapping. |
|
319 - DList is split into DList_Impl, DList, and DList_Cset. |
|
320 - Cset is split into Cset and List_Cset. |
|
321 |
|
322 * Theory Library/Nat_Infinity has been renamed to |
|
323 Library/Extended_Nat, with name changes of the following types and |
|
324 constants: |
|
325 |
|
326 type inat ~> type enat |
|
327 Fin ~> enat |
|
328 Infty ~> infinity (overloaded) |
|
329 iSuc ~> eSuc |
|
330 the_Fin ~> the_enat |
|
331 |
|
332 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has |
|
333 been renamed accordingly. INCOMPATIBILITY. |
|
334 |
|
335 * Session Multivariate_Analysis: The euclidean_space type class now |
|
336 fixes a constant "Basis :: 'a set" consisting of the standard |
|
337 orthonormal basis for the type. Users now have the option of |
|
338 quantifying over this set instead of using the "basis" function, e.g. |
|
339 "ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)". |
|
340 |
|
341 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed |
|
342 to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants |
|
343 "Cart_nth" and "Cart_lambda" have been respectively renamed to |
|
344 "vec_nth" and "vec_lambda"; theorems mentioning those names have |
|
345 changed to match. Definition theorems for overloaded constants now use |
|
346 the standard "foo_vec_def" naming scheme. A few other theorems have |
|
347 been renamed as follows (INCOMPATIBILITY): |
|
348 |
|
349 Cart_eq ~> vec_eq_iff |
|
350 dist_nth_le_cart ~> dist_vec_nth_le |
|
351 tendsto_vector ~> vec_tendstoI |
|
352 Cauchy_vector ~> vec_CauchyI |
|
353 |
|
354 * Session Multivariate_Analysis: Several duplicate theorems have been |
|
355 removed, and other theorems have been renamed or replaced with more |
|
356 general versions. INCOMPATIBILITY. |
|
357 |
|
358 finite_choice ~> finite_set_choice |
|
359 eventually_conjI ~> eventually_conj |
|
360 eventually_and ~> eventually_conj_iff |
|
361 eventually_false ~> eventually_False |
|
362 setsum_norm ~> norm_setsum |
|
363 Lim_sequentially ~> LIMSEQ_def |
|
364 Lim_ident_at ~> LIM_ident |
|
365 Lim_const ~> tendsto_const |
|
366 Lim_cmul ~> tendsto_scaleR [OF tendsto_const] |
|
367 Lim_neg ~> tendsto_minus |
|
368 Lim_add ~> tendsto_add |
|
369 Lim_sub ~> tendsto_diff |
|
370 Lim_mul ~> tendsto_scaleR |
|
371 Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] |
|
372 Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] |
|
373 Lim_linear ~> bounded_linear.tendsto |
|
374 Lim_component ~> tendsto_euclidean_component |
|
375 Lim_component_cart ~> tendsto_vec_nth |
|
376 Lim_inner ~> tendsto_inner [OF tendsto_const] |
|
377 dot_lsum ~> inner_setsum_left |
|
378 dot_rsum ~> inner_setsum_right |
|
379 continuous_cmul ~> continuous_scaleR [OF continuous_const] |
|
380 continuous_neg ~> continuous_minus |
|
381 continuous_sub ~> continuous_diff |
|
382 continuous_vmul ~> continuous_scaleR [OF _ continuous_const] |
|
383 continuous_mul ~> continuous_scaleR |
|
384 continuous_inv ~> continuous_inverse |
|
385 continuous_at_within_inv ~> continuous_at_within_inverse |
|
386 continuous_at_inv ~> continuous_at_inverse |
|
387 continuous_at_norm ~> continuous_norm [OF continuous_at_id] |
|
388 continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] |
|
389 continuous_at_component ~> continuous_component [OF continuous_at_id] |
|
390 continuous_on_neg ~> continuous_on_minus |
|
391 continuous_on_sub ~> continuous_on_diff |
|
392 continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] |
|
393 continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] |
|
394 continuous_on_mul ~> continuous_on_scaleR |
|
395 continuous_on_mul_real ~> continuous_on_mult |
|
396 continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] |
|
397 continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] |
|
398 continuous_on_inverse ~> continuous_on_inv |
|
399 uniformly_continuous_on_neg ~> uniformly_continuous_on_minus |
|
400 uniformly_continuous_on_sub ~> uniformly_continuous_on_diff |
|
401 subset_interior ~> interior_mono |
|
402 subset_closure ~> closure_mono |
|
403 closure_univ ~> closure_UNIV |
|
404 real_arch_lt ~> reals_Archimedean2 |
|
405 real_arch ~> reals_Archimedean3 |
|
406 real_abs_norm ~> abs_norm_cancel |
|
407 real_abs_sub_norm ~> norm_triangle_ineq3 |
|
408 norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 |
|
409 |
|
410 * Session HOL-Probability: |
|
411 - Caratheodory's extension lemma is now proved for ring_of_sets. |
|
412 - Infinite products of probability measures are now available. |
|
413 - Sigma closure is independent, if the generator is independent |
|
414 - Use extended reals instead of positive extended |
|
415 reals. INCOMPATIBILITY. |
|
416 |
420 |
417 |
421 *** Document preparation *** |
418 *** Document preparation *** |
422 |
419 |
423 * Antiquotation @{rail} layouts railroad syntax diagrams, see also |
420 * Antiquotation @{rail} layouts railroad syntax diagrams, see also |
424 isar-ref manual, both for description and actual application of the |
421 isar-ref manual, both for description and actual application of the |