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 |
11 |
12 * HOL: exhaust_tac on datatypes superceded by new case_tac; |
12 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
13 |
13 |
14 * ML: PureThy.add_thms/add_axioms/add_defs now return theorems; |
14 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; |
15 |
15 |
16 |
16 |
17 *** Document preparation *** |
17 *** Document preparation *** |
18 |
18 |
19 * isatool mkdir provides easy setup of Isabelle session directories, |
19 * isatool mkdir provides easy setup of Isabelle session directories, |
20 including proper documents; |
20 including proper document sources; |
21 |
21 |
22 * generated LaTeX sources are now deleted after successful run |
22 * generated LaTeX sources are now deleted after successful run |
23 (isatool document -c); may retain a copy somewhere else via -D option |
23 (isatool document -c); may retain a copy somewhere else via -D option |
24 of isatool usedir; |
24 of isatool usedir; |
25 |
25 |
26 * old-style theories now produce (crude) LaTeX sources as well; |
26 * old-style theories now produce (crude) LaTeX output as well; |
27 |
27 |
28 |
28 |
29 *** Isar *** |
29 *** Isar *** |
30 |
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 * Pure: new 'obtain' language element supports generalized existence |
35 * Pure: new 'obtain' language element supports generalized elimination |
36 proofs; |
36 proofs; |
37 |
37 |
38 * Pure: scalable support for case-analysis type proofs: new 'case' |
38 * Pure: scalable support for case-analysis type proofs: new 'case' |
39 language element refers to local contexts symbolically, as produced by |
39 language element refers to local contexts symbolically, as produced by |
40 certain proof methods; internally, case names are attached to theorems |
40 certain proof methods; internally, case names are attached to theorems |
51 * HOL: removed 'case_split' thm binding, should use 'cases' proof |
51 * HOL: removed 'case_split' thm binding, should use 'cases' proof |
52 method anyway; |
52 method anyway; |
53 |
53 |
54 * names of theorems etc. may be natural numbers as well; |
54 * names of theorems etc. may be natural numbers as well; |
55 |
55 |
56 * intro/elim/dest attributes: changed ! / !! flags to ? / ??; |
56 * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??; |
57 |
57 |
58 * 'pr' command: optional goals_limit argument; |
58 * 'pr' command: optional goals_limit argument; |
59 |
59 |
60 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit |
60 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit |
61 additional print modes to be specified; e.g. pr(latex) will print |
61 additional print modes to be specified; e.g. "pr(latex)" will print |
62 proof according to the Isabelle LaTeX style; |
62 proof state according to the Isabelle LaTeX style; |
63 |
63 |
64 |
64 |
65 *** HOL *** |
65 *** HOL *** |
66 |
66 |
67 * Algebra: new theory of rings and univariate polynomials, by Clemens |
67 * HOL/Algebra: new theory of rings and univariate polynomials, by |
68 Ballarin; |
68 Clemens Ballarin; |
69 |
69 |
70 * HOL/record: fixed select-update simplification procedure to handle |
70 * HOL/record: fixed select-update simplification procedure to handle |
71 extended records as well; admit "r" as field name; |
71 extended records as well; admit "r" as field name; |
72 |
72 |
73 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
73 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
74 Arithmetic, by Thomas M Rasmussen; |
74 Arithmetic, by Thomas M Rasmussen; |
75 |
75 |
76 * new version of "case_tac" subsumes both boolean case split and |
76 * new version of "case_tac" subsumes both boolean case split and |
77 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
77 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
78 exists, may define val exhaust_tac = case_tac for quick-and-dirty |
78 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
79 portability; |
|
80 |
79 |
81 |
80 |
82 *** General *** |
81 *** General *** |
83 |
82 |
84 * compression of ML heaps images may now be controlled via -c option |
83 * compression of ML heaps images may now be controlled via -c option |
85 of isabelle and isatool usedir; |
84 of isabelle and isatool usedir (currently only observed by Poly/ML); |
86 |
85 |
87 * new ML combinators |>> and |>>> for incremental transformations with |
86 * ML: new combinators |>> and |>>> for incremental transformations |
88 secondary results (e.g. certain theory extensions): |
87 with secondary results (e.g. certain theory extensions): |
89 |
|
90 |
88 |
91 |
89 |
92 |
90 |
93 New in Isabelle99 (October 1999) |
91 New in Isabelle99 (October 1999) |
94 -------------------------------- |
92 -------------------------------- |