12 * HOL: exhaust_tac on datatypes superceded by new case_tac; |
12 * HOL: exhaust_tac on datatypes superceded by new 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 now return theorems; |
15 |
15 |
16 |
16 |
17 *** Isabelle 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 documents; |
21 |
21 |
22 * generated LaTeX sources are now deleted after successful run |
22 * generated LaTeX sources are now deleted after successful run |
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 existence |
36 proofs; |
36 proofs; |
37 |
37 |
38 * Pure: much better 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 |
41 as "tags"; |
41 as "tags"; |
42 |
42 |
|
43 * Provers: splitter support (via 'split' attribute and 'simp' method |
|
44 modifier); 'simp' method: 'only:' modifier removes loopers as well |
|
45 (including splits); |
|
46 |
43 * HOL: new proof method 'cases' and improved version of 'induct' now |
47 * HOL: new proof method 'cases' and improved version of 'induct' now |
44 support named cases; major packages (inductive, datatype, primrec, |
48 support named cases; major packages (inductive, datatype, primrec, |
45 recdef) support case names and properly name parameters; |
49 recdef) support case names and properly name parameters; |
46 |
50 |
47 * HOL: removed 'case_split' thm binding, should use 'cases' proof |
51 * HOL: removed 'case_split' thm binding, should use 'cases' proof |
48 method anyway; |
52 method anyway; |
49 |
53 |
50 * names of theorems etc. may be natural numbers as well; |
54 * names of theorems etc. may be natural numbers as well; |
51 |
55 |
52 * intro/elim/dest attributes: changed ! / !! flags to ? / ??; |
56 * intro/elim/dest attributes: changed ! / !! flags to ? / ??; |
|
57 |
|
58 * 'pr' command: optional goals_limit argument; |
|
59 |
|
60 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit |
|
61 additional print modes to be specified; e.g. pr(latex) will print |
|
62 proof according to the Isabelle LaTeX style; |
53 |
63 |
54 |
64 |
55 *** HOL *** |
65 *** HOL *** |
56 |
66 |
57 * Algebra: new theory of rings and univariate polynomials, by Clemens |
67 * Algebra: new theory of rings and univariate polynomials, by Clemens |