6 |
6 |
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** General *** |
10 *** General *** |
|
11 |
|
12 * Command 'bundle' provides a local theory target to define a bundle |
|
13 from the body of specification commands (such as 'declare', |
|
14 'declaration', 'notation', 'lemmas', 'lemma'). For example: |
|
15 |
|
16 bundle foo |
|
17 begin |
|
18 declare a [simp] |
|
19 declare b [intro] |
|
20 end |
|
21 |
|
22 * Command 'unbundle' is like 'include', but works within a local theory |
|
23 context. Unlike "context includes ... begin", the effect of 'unbundle' |
|
24 on the target context persists, until different declarations are given. |
|
25 |
|
26 * Simplified outer syntax: uniform category "name" includes long |
|
27 identifiers. Former "xname" / "nameref" / "name reference" has been |
|
28 discontinued. |
11 |
29 |
12 * Embedded content (e.g. the inner syntax of types, terms, props) may be |
30 * Embedded content (e.g. the inner syntax of types, terms, props) may be |
13 delimited uniformly via cartouches. This works better than old-fashioned |
31 delimited uniformly via cartouches. This works better than old-fashioned |
14 quotes when sub-languages are nested. |
32 quotes when sub-languages are nested. |
15 |
|
16 * Type-inference improves sorts of newly introduced type variables for |
|
17 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL). |
|
18 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context |
|
19 produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare |
|
20 INCOMPATIBILITY, need to provide explicit type constraints for Pure |
|
21 types where this is really intended. |
|
22 |
|
23 * Simplified outer syntax: uniform category "name" includes long |
|
24 identifiers. Former "xname" / "nameref" / "name reference" has been |
|
25 discontinued. |
|
26 |
33 |
27 * Mixfix annotations support general block properties, with syntax |
34 * Mixfix annotations support general block properties, with syntax |
28 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", |
35 "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", |
29 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent |
36 "unbreakable", "markup". The existing notation "(DIGITS" is equivalent |
30 to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks |
37 to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks |
31 is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY. |
38 is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY. |
32 |
39 |
33 * Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> -- |
|
34 this allows special forms of document output. |
|
35 |
|
36 * Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control |
|
37 symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its |
|
38 derivatives. |
|
39 |
|
40 * \<^raw:...> symbols are no longer supported. |
|
41 |
|
42 * New symbol \<circle>, e.g. for temporal operator. |
|
43 |
|
44 * Old 'header' command is no longer supported (legacy since |
|
45 Isabelle2015). |
|
46 |
|
47 * Command 'bundle' provides a local theory target to define a bundle |
|
48 from the body of specification commands (such as 'declare', |
|
49 'declaration', 'notation', 'lemmas', 'lemma'). For example: |
|
50 |
|
51 bundle foo |
|
52 begin |
|
53 declare a [simp] |
|
54 declare b [intro] |
|
55 end |
|
56 |
|
57 * Command 'unbundle' is like 'include', but works within a local theory |
|
58 context. Unlike "context includes ... begin", the effect of 'unbundle' |
|
59 on the target context persists, until different declarations are given. |
|
60 |
|
61 * Splitter in simp, auto and friends: |
|
62 - The syntax "split add" has been discontinued, use plain "split". |
|
63 - For situations with many conditional or case expressions, |
|
64 there is an alternative splitting strategy that can be much faster. |
|
65 It is selected by writing "split!" instead of "split". It applies |
|
66 safe introduction and elimination rules after each split rule. |
|
67 As a result the subgoal may be split into several subgoals. |
|
68 |
|
69 * Proof method "blast" is more robust wrt. corner cases of Pure |
40 * Proof method "blast" is more robust wrt. corner cases of Pure |
70 statements without object-logic judgment. |
41 statements without object-logic judgment. |
71 |
42 |
72 * Pure provides basic versions of proof methods "simp" and "simp_all" |
|
73 that only know about meta-equality (==). Potential INCOMPATIBILITY in |
|
74 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order |
|
75 is relevant to avoid confusion of Pure.simp vs. HOL.simp. |
|
76 |
|
77 * Commands 'prf' and 'full_prf' are somewhat more informative (again): |
43 * Commands 'prf' and 'full_prf' are somewhat more informative (again): |
78 proof terms are reconstructed and cleaned from administrative thm |
44 proof terms are reconstructed and cleaned from administrative thm nodes. |
79 nodes. |
45 |
80 |
46 * Code generator: config option "code_timing" triggers measurements of |
81 * The command 'unfolding' and proof method "unfold" include a second |
47 different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
82 stage where given equations are passed through the attribute "abs_def" |
48 examples. |
83 before rewriting. This ensures that definitions are fully expanded, |
49 |
84 regardless of the actual parameters that are provided. Rare |
50 * Code generator: implicits in Scala (stemming from type class |
85 INCOMPATIBILITY in some corner cases: use proof method (simp only:) |
51 instances) are generated into companion object of corresponding type |
86 instead, or declare [[unfold_abs_def = false]] in the proof context. |
52 class, to resolve some situations where ambiguities may occur. |
|
53 |
|
54 * Splitter in simp, auto and friends: |
|
55 - The syntax "split add" has been discontinued, use plain "split", |
|
56 INCOMPATIBILITY. |
|
57 - For situations with many conditional or case expressions, there is |
|
58 an alternative splitting strategy that can be much faster. It is |
|
59 selected by writing "split!" instead of "split". It applies safe |
|
60 introduction and elimination rules after each split rule. As a |
|
61 result the subgoal may be split into several subgoals. |
87 |
62 |
88 |
63 |
89 *** Prover IDE -- Isabelle/Scala/jEdit *** |
64 *** Prover IDE -- Isabelle/Scala/jEdit *** |
|
65 |
|
66 * Highlighting of entity def/ref positions wrt. cursor. |
|
67 |
|
68 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all |
|
69 occurences of the formal entity at the caret position. This facilitates |
|
70 systematic renaming. |
|
71 |
|
72 * PIDE document markup works across multiple Isar commands, e.g. the |
|
73 results established at the end of a proof are properly identified in the |
|
74 theorem statement. |
|
75 |
|
76 * Cartouche abbreviations work both for " and ` to accomodate typical |
|
77 situations where old ASCII notation may be updated. |
90 |
78 |
91 * Dockable window "Symbols" also provides access to 'abbrevs' from the |
79 * Dockable window "Symbols" also provides access to 'abbrevs' from the |
92 outer syntax of the current theory buffer. This provides clickable |
80 outer syntax of the current theory buffer. This provides clickable |
93 syntax templates, including entries with empty abbrevs name (which are |
81 syntax templates, including entries with empty abbrevs name (which are |
94 inaccessible via keyboard completion). |
82 inaccessible via keyboard completion). |
95 |
|
96 * Cartouche abbreviations work both for " and ` to accomodate typical |
|
97 situations where old ASCII notation may be updated. |
|
98 |
|
99 * Isabelle/ML and Standard ML files are presented in Sidekick with the |
|
100 tree structure of section headings: this special comment format is |
|
101 described in "implementation" chapter 0, e.g. (*** section ***). |
|
102 |
83 |
103 * IDE support for the Isabelle/Pure bootstrap process, with the |
84 * IDE support for the Isabelle/Pure bootstrap process, with the |
104 following independent stages: |
85 following independent stages: |
105 |
86 |
106 src/Pure/ROOT0.ML |
87 src/Pure/ROOT0.ML |
136 number of subgoals. This requires information of ongoing document |
115 number of subgoals. This requires information of ongoing document |
137 processing and may thus lag behind, when the user is editing too |
116 processing and may thus lag behind, when the user is editing too |
138 quickly; see also option "jedit_script_indent" and |
117 quickly; see also option "jedit_script_indent" and |
139 "jedit_script_indent_limit". |
118 "jedit_script_indent_limit". |
140 |
119 |
141 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all |
120 * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' |
142 occurences of the formal entity at the caret position. This facilitates |
121 are treated as delimiters for fold structure; 'begin' and 'end' |
143 systematic renaming. |
122 structure of theory specifications is treated as well. |
144 |
123 |
145 * Action "isabelle.keymap-merge" asks the user to resolve pending |
124 * Action "isabelle.keymap-merge" asks the user to resolve pending |
146 Isabelle keymap changes that are in conflict with the current jEdit |
125 Isabelle keymap changes that are in conflict with the current jEdit |
147 keymap; non-conflicting changes are always applied implicitly. This |
126 keymap; non-conflicting changes are always applied implicitly. This |
148 action is automatically invoked on Isabelle/jEdit startup and thus |
127 action is automatically invoked on Isabelle/jEdit startup and thus |
149 increases chances that users see new keyboard shortcuts when re-using |
128 increases chances that users see new keyboard shortcuts when re-using |
150 old keymaps. |
129 old keymaps. |
151 |
130 |
152 * Document markup works across multiple Isar commands, e.g. the results |
|
153 established at the end of a proof are properly identified in the theorem |
|
154 statement. |
|
155 |
|
156 * Command 'proof' provides information about proof outline with cases, |
131 * Command 'proof' provides information about proof outline with cases, |
157 e.g. for proof methods "cases", "induct", "goal_cases". |
132 e.g. for proof methods "cases", "induct", "goal_cases". |
158 |
133 |
159 * Completion templates for commands involving "begin ... end" blocks, |
134 * Completion templates for commands involving "begin ... end" blocks, |
160 e.g. 'context', 'notepad'. |
135 e.g. 'context', 'notepad'. |
224 expression, e.g. |
213 expression, e.g. |
225 |
214 |
226 (use facts in simp) |
215 (use facts in simp) |
227 (use facts in \<open>simp add: ...\<close>) |
216 (use facts in \<open>simp add: ...\<close>) |
228 |
217 |
|
218 * The old proof method "default" has been removed (legacy since |
|
219 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
|
220 |
229 |
221 |
230 *** Pure *** |
222 *** Pure *** |
231 |
223 |
232 * Code generator: config option "code_timing" triggers measurements of |
224 * Pure provides basic versions of proof methods "simp" and "simp_all" |
233 different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
225 that only know about meta-equality (==). Potential INCOMPATIBILITY in |
234 examples. |
226 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order |
235 |
227 is relevant to avoid confusion of Pure.simp vs. HOL.simp. |
236 * Code generator: implicits in Scala (stemming from type class instances) |
228 |
237 are generated into companion object of corresponding type class, to resolve |
229 * The command 'unfolding' and proof method "unfold" include a second |
238 some situations where ambiguities may occur. |
230 stage where given equations are passed through the attribute "abs_def" |
|
231 before rewriting. This ensures that definitions are fully expanded, |
|
232 regardless of the actual parameters that are provided. Rare |
|
233 INCOMPATIBILITY in some corner cases: use proof method (simp only:) |
|
234 instead, or declare [[unfold_abs_def = false]] in the proof context. |
|
235 |
|
236 * Type-inference improves sorts of newly introduced type variables for |
|
237 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL). |
|
238 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context |
|
239 produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare |
|
240 INCOMPATIBILITY, need to provide explicit type constraints for Pure |
|
241 types where this is really intended. |
239 |
242 |
240 |
243 |
241 *** HOL *** |
244 *** HOL *** |
242 |
245 |
243 * New proof method "argo" using the built-in Argo solver based on SMT technology. |
246 * New proof method "argo" using the built-in Argo solver based on SMT |
244 The method can be used to prove goals of quantifier-free propositional logic, |
247 technology. The method can be used to prove goals of quantifier-free |
245 goals based on a combination of quantifier-free propositional logic with equality, |
248 propositional logic, goals based on a combination of quantifier-free |
246 and goals based on a combination of quantifier-free propositional logic with |
249 propositional logic with equality, and goals based on a combination of |
247 linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for |
250 quantifier-free propositional logic with linear real arithmetic |
248 examples. |
251 including min/max/abs. See HOL/ex/Argo_Examples.thy for examples. |
249 |
252 |
250 * Type class "div" with operation "mod" renamed to type class "modulo" with |
253 * Metis: The problem encoding has changed very slightly. This might |
251 operation "modulo", analogously to type class "divide". This eliminates the |
|
252 need to qualify any of those names in the presence of infix "mod" syntax. |
|
253 INCOMPATIBILITY. |
|
254 |
|
255 * The unique existence quantifier no longer provides 'binder' syntax, |
|
256 but uses syntax translations (as for bounded unique existence). Thus |
|
257 iterated quantification \<exists>!x y. P x y with its slightly confusing |
|
258 sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead, |
|
259 pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y |
|
260 (analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential |
|
261 INCOMPATIBILITY in rare situations. |
|
262 |
|
263 * Renamed session HOL-Multivariate_Analysis to HOL-Analysis. |
|
264 |
|
265 * Moved measure theory from HOL-Probability to HOL-Analysis. When importing |
|
266 HOL-Analysis some theorems need additional name spaces prefixes due to name |
|
267 clashes. |
|
268 INCOMPATIBILITY. |
|
269 |
|
270 * In HOL-Probability the type of emeasure and nn_integral was changed |
|
271 from ereal to ennreal: |
|
272 emeasure :: 'a measure => 'a set => ennreal |
|
273 nn_integral :: 'a measure => ('a => ennreal) => ennreal |
|
274 INCOMPATIBILITY. |
|
275 |
|
276 * HOL-Analysis: more complex analysis including Cauchy's inequality, Liouville theorem, |
|
277 open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma. |
|
278 |
|
279 * HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman |
|
280 Minkowski theorem. |
|
281 |
|
282 * HOL-Analysis: Numerous results ported from the HOL Light libraries: homeomorphisms, |
|
283 continuous function extensions and other advanced topics in topology |
|
284 |
|
285 * Number_Theory: algebraic foundation for primes: Generalisation of |
|
286 predicate "prime" and introduction of predicates "prime_elem", |
|
287 "irreducible", a "prime_factorization" function, and the "factorial_ring" |
|
288 typeclass with instance proofs for nat, int, poly. Some theorems now have |
|
289 different names, most notably "prime_def" is now "prime_nat_iff". |
|
290 INCOMPATIBILITY. |
|
291 |
|
292 * Probability: Code generation and QuickCheck for Probability Mass |
|
293 Functions. |
|
294 |
|
295 * Theory Set_Interval.thy: substantial new theorems on indexed sums |
|
296 and products. |
|
297 |
|
298 * Theory List.thy: |
|
299 listsum ~> sum_list |
|
300 listprod ~> prod_list |
|
301 |
|
302 * Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying |
|
303 equations in functional programming style: variables present on the |
|
304 left-hand but not on the righ-hand side are replaced by underscores. |
|
305 |
|
306 * "surj" is a mere input abbreviation, to avoid hiding an equation in |
|
307 term output. Minor INCOMPATIBILITY. |
|
308 |
|
309 * Theory Library/Combinator_PER.thy: combinator to build partial |
|
310 equivalence relations from a predicate and an equivalence relation. |
|
311 |
|
312 * Theory Library/Perm.thy: basic facts about almost everywhere fix |
|
313 bijections. |
|
314 |
|
315 * Theory Library/Normalized_Fraction.thy: allows viewing an element |
|
316 of a field of fractions as a normalized fraction (i.e. a pair of |
|
317 numerator and denominator such that the two are coprime and the |
|
318 denominator is normalized w.r.t. unit factors) |
|
319 |
|
320 * Locale bijection establishes convenient default simp rules |
|
321 like "inv f (f a) = a" for total bijections. |
|
322 |
|
323 * Former locale lifting_syntax is now a bundle, which is easier to |
|
324 include in a local context or theorem statement, e.g. "context includes |
|
325 lifting_syntax begin ... end". Minor INCOMPATIBILITY. |
|
326 |
|
327 * Code generation for scala: ambiguous implicts in class diagrams |
|
328 are spelt out explicitly. |
|
329 |
|
330 * Abstract locales semigroup, abel_semigroup, semilattice, |
|
331 semilattice_neutr, ordering, ordering_top, semilattice_order, |
|
332 semilattice_neutr_order, comm_monoid_set, semilattice_set, |
|
333 semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set |
|
334 monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset, |
|
335 comm_monoid_fun use boldified syntax uniformly that does not clash |
|
336 with corresponding global syntax. INCOMPATIBILITY. |
|
337 |
|
338 * Conventional syntax "%(). t" for unit abstractions. Slight syntactic |
|
339 INCOMPATIBILITY. |
|
340 |
|
341 * Command 'code_reflect' accepts empty constructor lists for datatypes, |
|
342 which renders those abstract effectively. |
|
343 |
|
344 * Command 'export_code' checks given constants for abstraction violations: |
|
345 a small guarantee that given constants specify a safe interface for the |
|
346 generated code. |
|
347 |
|
348 * Probability/Random_Permutations.thy contains some theory about |
|
349 choosing a permutation of a set uniformly at random and folding over a |
|
350 list in random order. |
|
351 |
|
352 * Probability/SPMF formalises discrete subprobability distributions. |
|
353 |
|
354 * Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax" |
|
355 allow to control optional syntax in local contexts; this supersedes |
|
356 former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle |
|
357 finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax". |
|
358 |
|
359 * Library/Set_Permutations.thy (executably) defines the set of |
|
360 permutations of a set, i.e. the set of all lists that contain every |
|
361 element of the carrier set exactly once. |
|
362 |
|
363 * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on |
|
364 explicitly provided auxiliary definitions for required type class |
|
365 dictionaries rather than half-working magic. INCOMPATIBILITY, see |
|
366 the tutorial on code generation for details. |
|
367 |
|
368 * New abbreviations for negated existence (but not bounded existence): |
|
369 |
|
370 \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) |
|
371 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
|
372 |
|
373 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
|
374 has been removed for output. It is retained for input only, until it is |
|
375 eliminated altogether. |
|
376 |
|
377 * metis: The problem encoding has changed very slightly. This might |
|
378 break existing proofs. INCOMPATIBILITY. |
254 break existing proofs. INCOMPATIBILITY. |
379 |
255 |
380 * Sledgehammer: |
256 * Sledgehammer: |
381 - The MaSh relevance filter is now faster than before. |
257 - The MaSh relevance filter is now faster than before. |
382 - Produce syntactically correct Vampire 4.0 problem files. |
258 - Produce syntactically correct Vampire 4.0 problem files. |
383 |
|
384 * The 'coinductive' command produces a proper coinduction rule for |
|
385 mutual coinductive predicates. This new rule replaces the old rule, |
|
386 which exposed details of the internal fixpoint construction and was |
|
387 hard to use. INCOMPATIBILITY. |
|
388 |
259 |
389 * (Co)datatype package: |
260 * (Co)datatype package: |
390 - New commands for defining corecursive functions and reasoning about |
261 - New commands for defining corecursive functions and reasoning about |
391 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
262 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
392 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
263 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
393 method. See 'isabelle doc corec'. |
264 method. See 'isabelle doc corec'. |
394 - The predicator :: ('a => bool) => 'a F => bool is now a first-class |
265 - The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a first-class |
395 citizen in bounded natural functors. |
266 citizen in bounded natural functors. |
396 - 'primrec' now allows nested calls through the predicator in addition |
267 - 'primrec' now allows nested calls through the predicator in addition |
397 to the map function. |
268 to the map function. |
398 - 'bnf' automatically discharges reflexive proof obligations. |
269 - 'bnf' automatically discharges reflexive proof obligations. |
399 - 'bnf' outputs a slightly modified proof obligation expressing rel in |
270 - 'bnf' outputs a slightly modified proof obligation expressing rel in |
409 - The "size" plugin has been made compatible again with locales. |
280 - The "size" plugin has been made compatible again with locales. |
410 - The theorems about "rel" and "set" may have a slightly different (but |
281 - The theorems about "rel" and "set" may have a slightly different (but |
411 equivalent) form. |
282 equivalent) form. |
412 INCOMPATIBILITY. |
283 INCOMPATIBILITY. |
413 |
284 |
414 * Some old / obsolete theorems have been renamed / removed, potential |
285 * The 'coinductive' command produces a proper coinduction rule for |
415 INCOMPATIBILITY. |
286 mutual coinductive predicates. This new rule replaces the old rule, |
416 |
287 which exposed details of the internal fixpoint construction and was |
417 nat_less_cases -- removed, use linorder_cases instead |
288 hard to use. INCOMPATIBILITY. |
418 inv_image_comp -- removed, use image_inv_f_f instead |
289 |
419 image_surj_f_inv_f ~> image_f_inv_f |
290 * New abbreviations for negated existence (but not bounded existence): |
420 |
291 |
421 * Some theorems about groups and orders have been generalised from |
292 \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) |
422 groups to semi-groups that are also monoids: |
293 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
423 le_add_same_cancel1 |
294 |
424 le_add_same_cancel2 |
295 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
425 less_add_same_cancel1 |
296 has been removed for output. It is retained for input only, until it is |
426 less_add_same_cancel2 |
297 eliminated altogether. |
427 add_le_same_cancel1 |
298 |
428 add_le_same_cancel2 |
299 * The unique existence quantifier no longer provides 'binder' syntax, |
429 add_less_same_cancel1 |
300 but uses syntax translations (as for bounded unique existence). Thus |
430 add_less_same_cancel2 |
301 iterated quantification \<exists>!x y. P x y with its slightly confusing |
431 |
302 sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead, |
432 * Some simplifications theorems about rings have been removed, since |
303 pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y |
433 superseeded by a more general version: |
304 (analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential |
434 less_add_cancel_left_greater_zero ~> less_add_same_cancel1 |
305 INCOMPATIBILITY in rare situations. |
435 less_add_cancel_right_greater_zero ~> less_add_same_cancel2 |
306 |
436 less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1 |
307 * Conventional syntax "%(). t" for unit abstractions. Slight syntactic |
437 less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2 |
308 INCOMPATIBILITY. |
438 less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1 |
|
439 less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2 |
|
440 less_add_cancel_left_less_zero ~> add_less_same_cancel1 |
|
441 less_add_cancel_right_less_zero ~> add_less_same_cancel2 |
|
442 INCOMPATIBILITY. |
|
443 |
|
444 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to |
|
445 resemble the f.split naming convention, INCOMPATIBILITY. |
|
446 |
309 |
447 * Characters (type char) are modelled as finite algebraic type |
310 * Characters (type char) are modelled as finite algebraic type |
448 corresponding to {0..255}. |
311 corresponding to {0..255}. |
449 |
312 |
450 - Logical representation: |
313 - Logical representation: |
466 provided as char_of_nat, nat_of_char (as before). |
329 provided as char_of_nat, nat_of_char (as before). |
467 - The auxiliary nibble type has been discontinued. |
330 - The auxiliary nibble type has been discontinued. |
468 |
331 |
469 INCOMPATIBILITY. |
332 INCOMPATIBILITY. |
470 |
333 |
471 * Multiset membership is now expressed using set_mset rather than count. |
334 * Type class "div" with operation "mod" renamed to type class "modulo" |
|
335 with operation "modulo", analogously to type class "divide". This |
|
336 eliminates the need to qualify any of those names in the presence of |
|
337 infix "mod" syntax. INCOMPATIBILITY. |
|
338 |
|
339 * Constant "surj" is a mere input abbreviation, to avoid hiding an |
|
340 equation in term output. Minor INCOMPATIBILITY. |
|
341 |
|
342 * Command 'code_reflect' accepts empty constructor lists for datatypes, |
|
343 which renders those abstract effectively. |
|
344 |
|
345 * Command 'export_code' checks given constants for abstraction |
|
346 violations: a small guarantee that given constants specify a safe |
|
347 interface for the generated code. |
|
348 |
|
349 * Code generation for Scala: ambiguous implicts in class diagrams are |
|
350 spelt out explicitly. |
|
351 |
|
352 * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on |
|
353 explicitly provided auxiliary definitions for required type class |
|
354 dictionaries rather than half-working magic. INCOMPATIBILITY, see |
|
355 the tutorial on code generation for details. |
|
356 |
|
357 * Theory Set_Interval.thy: substantial new theorems on indexed sums |
|
358 and products. |
|
359 |
|
360 * Theory List.thy: ranaming of listsum ~> sum_list, listprod ~> |
|
361 prod_list, INCOMPATIBILITY. |
|
362 |
|
363 * Locale bijection establishes convenient default simp rules such as |
|
364 "inv f (f a) = a" for total bijections. |
|
365 |
|
366 * Abstract locales semigroup, abel_semigroup, semilattice, |
|
367 semilattice_neutr, ordering, ordering_top, semilattice_order, |
|
368 semilattice_neutr_order, comm_monoid_set, semilattice_set, |
|
369 semilattice_neutr_set, semilattice_order_set, |
|
370 semilattice_order_neutr_set monoid_list, comm_monoid_list, |
|
371 comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified |
|
372 syntax uniformly that does not clash with corresponding global syntax. |
|
373 INCOMPATIBILITY. |
|
374 |
|
375 * Former locale lifting_syntax is now a bundle, which is easier to |
|
376 include in a local context or theorem statement, e.g. "context includes |
|
377 lifting_syntax begin ... end". Minor INCOMPATIBILITY. |
|
378 |
|
379 * Some old / obsolete theorems have been renamed / removed, potential |
|
380 INCOMPATIBILITY. |
|
381 |
|
382 nat_less_cases -- removed, use linorder_cases instead |
|
383 inv_image_comp -- removed, use image_inv_f_f instead |
|
384 image_surj_f_inv_f ~> image_f_inv_f |
|
385 |
|
386 * Some theorems about groups and orders have been generalised from |
|
387 groups to semi-groups that are also monoids: |
|
388 le_add_same_cancel1 |
|
389 le_add_same_cancel2 |
|
390 less_add_same_cancel1 |
|
391 less_add_same_cancel2 |
|
392 add_le_same_cancel1 |
|
393 add_le_same_cancel2 |
|
394 add_less_same_cancel1 |
|
395 add_less_same_cancel2 |
|
396 |
|
397 * Some simplifications theorems about rings have been removed, since |
|
398 superseeded by a more general version: |
|
399 less_add_cancel_left_greater_zero ~> less_add_same_cancel1 |
|
400 less_add_cancel_right_greater_zero ~> less_add_same_cancel2 |
|
401 less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1 |
|
402 less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2 |
|
403 less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1 |
|
404 less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2 |
|
405 less_add_cancel_left_less_zero ~> add_less_same_cancel1 |
|
406 less_add_cancel_right_less_zero ~> add_less_same_cancel2 |
|
407 INCOMPATIBILITY. |
|
408 |
|
409 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to |
|
410 resemble the f.split naming convention, INCOMPATIBILITY. |
|
411 |
|
412 * Added class topological_monoid. |
|
413 |
|
414 * HOL-Library: theory FinFun bundles "finfun_syntax" and |
|
415 "no_finfun_syntax" allow to control optional syntax in local contexts; |
|
416 this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use |
|
417 "unbundle finfun_syntax" to imitate import of |
|
418 "~~/src/HOL/Library/FinFun_Syntax". |
|
419 |
|
420 * HOL-Library: theory Set_Permutations (executably) defines the set of |
|
421 permutations of a set, i.e. the set of all lists that contain every |
|
422 element of the carrier set exactly once. |
|
423 |
|
424 * HOL-Library: multiset membership is now expressed using set_mset |
|
425 rather than count. |
472 |
426 |
473 - Expressions "count M a > 0" and similar simplify to membership |
427 - Expressions "count M a > 0" and similar simplify to membership |
474 by default. |
428 by default. |
475 |
429 |
476 - Converting between "count M a = 0" and non-membership happens using |
430 - Converting between "count M a = 0" and non-membership happens using |
482 - Rules count_in_diffI and in_diff_countE obtain facts of the form |
436 - Rules count_in_diffI and in_diff_countE obtain facts of the form |
483 "count M a = n + count N a" from membership on difference sets. |
437 "count M a = n + count N a" from membership on difference sets. |
484 |
438 |
485 INCOMPATIBILITY. |
439 INCOMPATIBILITY. |
486 |
440 |
487 * The names of multiset theorems have been normalised to distinguish which |
441 * HOL-Library: theory LaTeXsugar uses new-style "dummy_pats" for |
488 ordering the theorems are about |
442 displaying equations in functional programming style --- variables |
|
443 present on the left-hand but not on the righ-hand side are replaced by |
|
444 underscores. |
|
445 |
|
446 * HOL-Library: theory Combinator_PER provides combinator to build |
|
447 partial equivalence relations from a predicate and an equivalence |
|
448 relation. |
|
449 |
|
450 * HOL-Library: theory Perm provides basic facts about almost everywhere |
|
451 fix bijections. |
|
452 |
|
453 * HOL-Library: theory Normalized_Fraction allows viewing an element of a |
|
454 field of fractions as a normalized fraction (i.e. a pair of numerator |
|
455 and denominator such that the two are coprime and the denominator is |
|
456 normalized wrt. unit factors). |
|
457 |
|
458 * Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis. |
|
459 |
|
460 * Session HOL-Multivariate_Analysis has been renamed to HOL-Analysis. |
|
461 |
|
462 * HOL-Analysis: measure theory has been moved here from HOL-Probability. |
|
463 When importing HOL-Analysis some theorems need additional name spaces |
|
464 prefixes due to name clashes. INCOMPATIBILITY. |
|
465 |
|
466 * HOL-Analysis: more complex analysis including Cauchy's inequality, |
|
467 Liouville theorem, open mapping theorem, maximum modulus principle, |
|
468 Residue theorem, Schwarz Lemma. |
|
469 |
|
470 * HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, |
|
471 and the Krein–Milman Minkowski theorem. |
|
472 |
|
473 * HOL-Analysis: Numerous results ported from the HOL Light libraries: |
|
474 homeomorphisms, continuous function extensions and other advanced topics |
|
475 in topology |
|
476 |
|
477 * HOL-Probability: the type of emeasure and nn_integral was changed from |
|
478 ereal to ennreal, INCOMPATIBILITY. |
|
479 |
|
480 emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal |
|
481 nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal |
|
482 |
|
483 * HOL-Probability: Code generation and QuickCheck for Probability Mass |
|
484 Functions. |
|
485 |
|
486 * HOL-Probability: theory Random_Permutations contains some theory about |
|
487 choosing a permutation of a set uniformly at random and folding over a |
|
488 list in random order. |
|
489 |
|
490 * HOL-Probability: theory SPMF formalises discrete subprobability |
|
491 distributions. |
|
492 |
|
493 * HOL-Number_Theory: algebraic foundation for primes: Generalisation of |
|
494 predicate "prime" and introduction of predicates "prime_elem", |
|
495 "irreducible", a "prime_factorization" function, and the |
|
496 "factorial_ring" typeclass with instance proofs for nat, int, poly. Some |
|
497 theorems now have different names, most notably "prime_def" is now |
|
498 "prime_nat_iff". INCOMPATIBILITY. |
|
499 |
|
500 * HOL-Library: the names of multiset theorems have been normalised to |
|
501 distinguish which ordering the theorems are about |
|
502 |
489 mset_less_eqI ~> mset_subset_eqI |
503 mset_less_eqI ~> mset_subset_eqI |
490 mset_less_insertD ~> mset_subset_insertD |
504 mset_less_insertD ~> mset_subset_insertD |
491 mset_less_eq_count ~> mset_subset_eq_count |
505 mset_less_eq_count ~> mset_subset_eq_count |
492 mset_less_diff_self ~> mset_subset_diff_self |
506 mset_less_diff_self ~> mset_subset_diff_self |
493 mset_le_exists_conv ~> mset_subset_eq_exists_conv |
507 mset_le_exists_conv ~> mset_subset_eq_exists_conv |
510 wf_less_mset_rel ~> wf_subset_mset_rel |
524 wf_less_mset_rel ~> wf_subset_mset_rel |
511 count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq |
525 count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq |
512 mset_remdups_le ~> mset_remdups_subset_eq |
526 mset_remdups_le ~> mset_remdups_subset_eq |
513 ms_lesseq_impl ~> subset_eq_mset_impl |
527 ms_lesseq_impl ~> subset_eq_mset_impl |
514 |
528 |
515 Some functions have been renamed: |
529 Some functions have been renamed: |
516 ms_lesseq_impl -> subset_eq_mset_impl |
530 ms_lesseq_impl -> subset_eq_mset_impl |
517 |
531 |
518 * Multisets are now ordered with the multiset ordering |
532 * HOL-Library: multisets are now ordered with the multiset ordering |
519 #\<subseteq># ~> \<le> |
533 #\<subseteq># ~> \<le> |
520 #\<subset># ~> < |
534 #\<subset># ~> < |
521 le_multiset ~> less_eq_multiset |
535 le_multiset ~> less_eq_multiset |
522 less_multiset ~> le_multiset |
536 less_multiset ~> le_multiset |
523 INCOMPATIBILITY. |
537 INCOMPATIBILITY. |
524 |
538 |
525 * The prefix multiset_order has been discontinued: the theorems can be directly |
539 * HOL-Library: the prefix multiset_order has been discontinued: the |
526 accessed. As a consequence, the lemmas "order_multiset" and "linorder_multiset" |
540 theorems can be directly accessed. As a consequence, the lemmas |
527 have been discontinued, and the interpretations "multiset_linorder" and |
541 "order_multiset" and "linorder_multiset" have been discontinued, and the |
528 "multiset_wellorder" have been replaced by instantiations. |
542 interpretations "multiset_linorder" and "multiset_wellorder" have been |
529 INCOMPATIBILITY. |
543 replaced by instantiations. INCOMPATIBILITY. |
530 |
544 |
531 * Some theorems about the multiset ordering have been renamed: |
545 * HOL-Library: some theorems about the multiset ordering have been |
|
546 renamed: |
|
547 |
532 le_multiset_def ~> less_eq_multiset_def |
548 le_multiset_def ~> less_eq_multiset_def |
533 less_multiset_def ~> le_multiset_def |
549 less_multiset_def ~> le_multiset_def |
534 less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset |
550 less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset |
535 mult_less_not_refl ~> mset_le_not_refl |
551 mult_less_not_refl ~> mset_le_not_refl |
536 mult_less_trans ~> mset_le_trans |
552 mult_less_trans ~> mset_le_trans |
552 le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty |
568 le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty |
553 less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff |
569 less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff |
554 less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff |
570 less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff |
555 INCOMPATIBILITY. |
571 INCOMPATIBILITY. |
556 |
572 |
557 * The lemma mset_map has now the attribute [simp]. |
573 * HOL-Library: the lemma mset_map has now the attribute [simp]. |
558 INCOMPATIBILITY. |
574 INCOMPATIBILITY. |
559 |
575 |
560 * Some theorems about multisets have been removed: |
576 * HOL-Library: some theorems about multisets have been removed. |
|
577 INCOMPATIBILITY, use the following replacements: |
|
578 |
561 le_multiset_plus_plus_left_iff ~> add_less_cancel_right |
579 le_multiset_plus_plus_left_iff ~> add_less_cancel_right |
562 le_multiset_plus_plus_right_iff ~> add_less_cancel_left |
580 le_multiset_plus_plus_right_iff ~> add_less_cancel_left |
563 add_eq_self_empty_iff ~> add_cancel_left_right |
581 add_eq_self_empty_iff ~> add_cancel_left_right |
564 mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right |
582 mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right |
565 INCOMPATIBILITY. |
583 |
566 |
584 * HOL-Library: some typeclass constraints about multisets have been |
567 * Some typeclass constraints about multisets have been reduced from ordered or |
585 reduced from ordered or linordered to preorder. Multisets have the |
568 linordered to preorder. Multisets have the additional typeclasses order_bot, |
586 additional typeclasses order_bot, no_top, |
569 no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, |
587 ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, |
570 linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le. |
588 linordered_cancel_ab_semigroup_add, and |
571 INCOMPATIBILITY. |
589 ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. |
572 |
590 |
573 * There are some new simplification rules about multisets, the multiset |
591 * HOL-Library: there are some new simplification rules about multisets, |
574 ordering, and the subset ordering on multisets. |
592 the multiset ordering, and the subset ordering on multisets. |
575 INCOMPATIBILITY. |
593 INCOMPATIBILITY. |
576 |
594 |
577 * The subset ordering on multisets has now the interpretations |
595 * HOL-Library: the subset ordering on multisets has now the |
578 ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot. |
596 interpretations ordered_ab_semigroup_monoid_add_imp_le and |
579 INCOMPATIBILITY. |
597 bounded_lattice_bot. INCOMPATIBILITY. |
580 |
598 |
581 * Multiset: single has been removed in favor of add_mset that roughly |
599 * HOL-Library/Multiset: single has been removed in favor of add_mset |
582 corresponds to Set.insert. Some theorems have removed or changed: |
600 that roughly corresponds to Set.insert. Some theorems have removed or |
|
601 changed: |
|
602 |
583 single_not_empty ~> add_mset_not_empty or empty_not_add_mset |
603 single_not_empty ~> add_mset_not_empty or empty_not_add_mset |
584 fold_mset_insert ~> fold_mset_add_mset |
604 fold_mset_insert ~> fold_mset_add_mset |
585 image_mset_insert ~> image_mset_add_mset |
605 image_mset_insert ~> image_mset_add_mset |
586 union_single_eq_diff |
606 union_single_eq_diff |
587 multi_self_add_other_not_self |
607 multi_self_add_other_not_self |
588 diff_single_eq_union |
608 diff_single_eq_union |
589 INCOMPATIBILITY. |
609 INCOMPATIBILITY. |
590 |
610 |
591 * Multiset: some theorems have been changed to use add_mset instead of single: |
611 * HOL-Library/Multiset: some theorems have been changed to use add_mset |
|
612 instead of single: |
|
613 |
592 mset_add |
614 mset_add |
593 multi_self_add_other_not_self |
615 multi_self_add_other_not_self |
594 diff_single_eq_union |
616 diff_single_eq_union |
595 union_single_eq_diff |
617 union_single_eq_diff |
596 union_single_eq_member |
618 union_single_eq_member |
662 sup_empty [simp] ~> [] |
684 sup_empty [simp] ~> [] |
663 inter_empty [simp] ~> [] |
685 inter_empty [simp] ~> [] |
664 empty_inter [simp] ~> [] |
686 empty_inter [simp] ~> [] |
665 INCOMPATIBILITY. |
687 INCOMPATIBILITY. |
666 |
688 |
667 * The order of the variables in the second cases of multiset_induct, |
689 * HOL-Library/Multiset. The order of the variables in the second cases |
668 multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A). |
690 of multiset_induct, multiset_induct2_size, multiset_induct2 has been |
669 INCOMPATIBILITY. |
691 changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY. |
670 |
692 |
671 * There is now a simplification procedure on multisets. It mimics the behavior |
693 * HOL-Library/Multiset. There is now a simplification procedure on |
672 of the procedure on natural numbers. |
694 multisets. It mimics the behavior of the procedure on natural numbers. |
673 INCOMPATIBILITY. |
695 INCOMPATIBILITY. |
674 |
696 |
675 * Renamed sums and products of multisets: |
697 * HOL-Library/Multiset. Renamed sums and products of multisets: |
676 msetsum ~> sum_mset |
698 msetsum ~> sum_mset |
677 msetprod ~> prod_mset |
699 msetprod ~> prod_mset |
678 |
700 |
679 * The symbols for intersection and union of multisets have been changed: |
701 * HOL-Library/Multiset. The notation for intersection and union of |
|
702 multisets have been changed: |
680 #\<inter> ~> \<inter># |
703 #\<inter> ~> \<inter># |
681 #\<union> ~> \<union># |
704 #\<union> ~> \<union># |
682 INCOMPATIBILITY. |
705 INCOMPATIBILITY. |
683 |
706 |
684 * The lemma one_step_implies_mult_aux on multisets has been removed, use |
707 * HOL-Library/Multiset. The lemma one_step_implies_mult_aux on multisets |
685 one_step_implies_mult instead. |
708 has been removed, use one_step_implies_mult instead. INCOMPATIBILITY. |
686 INCOMPATIBILITY. |
|
687 |
709 |
688 * The following theorems have been renamed: |
710 * The following theorems have been renamed: |
689 setsum_left_distrib ~> setsum_distrib_right |
711 setsum_left_distrib ~> setsum_distrib_right |
690 setsum_right_distrib ~> setsum_distrib_left |
712 setsum_right_distrib ~> setsum_distrib_left |
691 INCOMPATIBILITY. |
713 INCOMPATIBILITY. |
697 comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". |
719 comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". |
698 |
720 |
699 * Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. |
721 * Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. |
700 |
722 |
701 * The type class ordered_comm_monoid_add is now called |
723 * The type class ordered_comm_monoid_add is now called |
702 ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is |
724 ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add |
703 introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add. |
725 is introduced as the combination of ordered_ab_semigroup_add + |
704 INCOMPATIBILITY. |
726 comm_monoid_add. INCOMPATIBILITY. |
705 |
727 |
706 * Introduced the type classes canonically_ordered_comm_monoid_add and dioid. |
728 * Introduced the type classes canonically_ordered_comm_monoid_add and |
|
729 dioid. |
707 |
730 |
708 * Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When |
731 * Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When |
709 instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit |
732 instantiating linordered_semiring_strict and ordered_ab_group_add, an |
710 instantiation of ordered_ab_semigroup_monoid_add_imp_le might be |
733 explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might |
711 required. |
734 be required. INCOMPATIBILITY. |
712 INCOMPATIBILITY. |
735 |
713 |
736 * HOL-Library: theory Complete_Partial_Order2 provides reasoning support |
714 * Added topological_monoid |
737 for monotonicity and continuity in chain-complete partial orders and |
715 |
738 about admissibility conditions for fixpoint inductions. |
716 * Library/Complete_Partial_Order2.thy provides reasoning support for |
739 |
717 proofs about monotonicity and continuity in chain-complete partial |
740 * HOL-Library: theory Polynomial contains also derivation of polynomials |
718 orders and about admissibility conditions for fixpoint inductions. |
741 but not gcd/lcm on polynomials over fields. This has been moved to a |
719 |
742 separate theory Library/Polynomial_GCD_euclidean.thy, to pave way for a |
720 * Library/Polynomial.thy contains also derivation of polynomials |
743 possible future different type class instantiation for polynomials over |
721 but not gcd/lcm on polynomials over fields. This has been moved |
744 factorial rings. INCOMPATIBILITY. |
722 to a separate theory Library/Polynomial_GCD_euclidean.thy, to |
745 |
723 pave way for a possible future different type class instantiation |
746 * HOL-Library: theory Sublist.thy provides function "prefixes" with the |
724 for polynomials over factorial rings. INCOMPATIBILITY. |
747 following renaming |
725 |
748 |
726 * Library/Sublist.thy: added function "prefixes" and renamed |
|
727 prefixeq -> prefix |
749 prefixeq -> prefix |
728 prefix -> strict_prefix |
750 prefix -> strict_prefix |
729 suffixeq -> suffix |
751 suffixeq -> suffix |
730 suffix -> strict_suffix |
752 suffix -> strict_suffix |
731 Added theory of longest common prefixes. |
753 |
|
754 Added theory of longest common prefixes. |
732 |
755 |
733 * Dropped various legacy fact bindings, whose replacements are often |
756 * Dropped various legacy fact bindings, whose replacements are often |
734 of a more general type also: |
757 of a more general type also: |
735 lcm_left_commute_nat ~> lcm.left_commute |
758 lcm_left_commute_nat ~> lcm.left_commute |
736 lcm_left_commute_int ~> lcm.left_commute |
759 lcm_left_commute_int ~> lcm.left_commute |