6 ---------------------------- |
6 ---------------------------- |
7 |
7 |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
9 |
9 |
10 * HOL: the constant for f``x is now "image" rather than "op ``". |
10 * HOL: the constant for f``x is now "image" rather than "op ``". |
|
11 |
|
12 * HOL: exhaust_tac on datatypes superceded by new case_tac; |
|
13 |
|
14 * ML: PureThy.add_thms/add_axioms/add_defs now return theorems; |
11 |
15 |
12 |
16 |
13 *** Isabelle document preparation *** |
17 *** Isabelle document preparation *** |
14 |
18 |
15 * isatool mkdir provides easy setup of Isabelle session directories, |
19 * isatool mkdir provides easy setup of Isabelle session directories, |
22 * old-style theories now produce (crude) LaTeX sources as well; |
26 * old-style theories now produce (crude) LaTeX sources as well; |
23 |
27 |
24 |
28 |
25 *** Isar *** |
29 *** Isar *** |
26 |
30 |
27 * names of theorems etc. may be natural numbers as well; |
|
28 |
|
29 * intro/elim/dest attributes: changed ! / !! flags to ? / ??; |
|
30 |
|
31 * Pure now provides its own version of intro/elim/dest attributes; |
31 * Pure now provides its own version of intro/elim/dest attributes; |
32 useful for building new logics, but beware of confusion with the |
32 useful for building new logics, but beware of confusion with the |
33 Provers/classical ones! |
33 Provers/classical ones! |
34 |
34 |
35 * new 'obtain' language element supports generalized existence proofs; |
35 * Pure: new 'obtain' language element supports generalized existence |
36 |
36 proofs; |
37 * HOL: removed "case_split" thm binding, should use "cases" proof |
37 |
|
38 * Pure: much better support for case-analysis type proofs: new 'case' |
|
39 language element refers to local contexts symbolically, as produced by |
|
40 certain proof methods; internally, case names are attached to theorems |
|
41 as "tags"; |
|
42 |
|
43 * HOL: new proof method 'cases' and improved version of 'induct' now |
|
44 support named cases; major packages (inductive, datatype, primrec, |
|
45 recdef) support case names and properly name parameters; |
|
46 |
|
47 * HOL: removed 'case_split' thm binding, should use 'cases' proof |
38 method anyway; |
48 method anyway; |
39 |
49 |
40 * tuned syntax of "induct" method; |
50 * names of theorems etc. may be natural numbers as well; |
41 |
51 |
42 * new "cases" method for propositions, inductive sets and types; |
52 * intro/elim/dest attributes: changed ! / !! flags to ? / ??; |
43 |
53 |
44 |
54 |
45 *** HOL *** |
55 *** HOL *** |
46 |
56 |
47 * Algebra: new theory of rings and univariate polynomials, by Clemens |
57 * Algebra: new theory of rings and univariate polynomials, by Clemens |
51 extended records as well; admit "r" as field name; |
61 extended records as well; admit "r" as field name; |
52 |
62 |
53 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
63 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
54 Arithmetic, by Thomas M Rasmussen; |
64 Arithmetic, by Thomas M Rasmussen; |
55 |
65 |
56 * There is a new tactic "cases_tac" for case distinctions; it subsumes the |
66 * new version of "case_tac" subsumes both boolean case split and |
57 old "case_tac" and "exhaust_tac" (which should no longer be used). |
67 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
|
68 exists, may define val exhaust_tac = case_tac for quick-and-dirty |
|
69 portability; |
|
70 |
58 |
71 |
59 *** General *** |
72 *** General *** |
60 |
73 |
61 * compression of ML heaps images may now be controlled via -c option |
74 * compression of ML heaps images may now be controlled via -c option |
62 of isabelle and isatool usedir; |
75 of isabelle and isatool usedir; |
|
76 |
|
77 * new ML combinators |>> and |>>> for incremental transformations with |
|
78 secondary results (e.g. certain theory extensions): |
|
79 |
63 |
80 |
64 |
81 |
65 |
82 |
66 New in Isabelle99 (October 1999) |
83 New in Isabelle99 (October 1999) |
67 -------------------------------- |
84 -------------------------------- |