equal
deleted
inserted
replaced
50 |
50 |
51 * HOL: qed_spec_mp now also removes bounded ALL; |
51 * HOL: qed_spec_mp now also removes bounded ALL; |
52 |
52 |
53 * ZF: new treatment of arithmetic (nat & int) may break some old proofs; |
53 * ZF: new treatment of arithmetic (nat & int) may break some old proofs; |
54 |
54 |
55 * Isar/Provers: intro/elim/dest attributes: changed |
55 * Isar/Provers: intro/elim/dest attributes changed; renamed |
56 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one |
56 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one |
57 should have to change intro!! to intro? only); replaced "delrule" by |
57 should have to change intro!! to intro? only); replaced "delrule" by |
58 "rule del"; |
58 "rule del"; |
59 |
59 |
60 * Isar: changed syntax of local blocks from {{ }} to { }; |
60 * Isar: changed syntax of local blocks from {{ }} to { }; |
61 |
61 |
62 * Isar: renamed 'RS' attribute to 'THEN'; |
62 * Isar: renamed 'RS' attribute to 'THEN'; |
63 |
63 |
64 * Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...); |
64 * Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...); |
65 |
65 |
66 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; |
66 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions; |
67 |
67 |
68 * Provers: strengthened force_tac by using new first_best_tac; |
68 * Provers: strengthened force_tac by using new first_best_tac; |
69 |
69 |
190 * HOL/inductive: rename "intrs" to "intros" (potential |
190 * HOL/inductive: rename "intrs" to "intros" (potential |
191 INCOMPATIBILITY); emulation of mk_cases feature for proof scripts: |
191 INCOMPATIBILITY); emulation of mk_cases feature for proof scripts: |
192 'inductive_cases' command and 'ind_cases' method; NOTE: use (cases |
192 'inductive_cases' command and 'ind_cases' method; NOTE: use (cases |
193 (simplified)) method in proper proofs; |
193 (simplified)) method in proper proofs; |
194 |
194 |
195 * Provers: intro/elim/dest attributes: changed intro/intro!/intro!! |
195 * Provers: intro/elim/dest attributes changed; renamed |
196 flags to intro!/intro/intro? (in most cases, one should have to change |
196 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in |
197 intro!! to intro? only); replaced "delrule" by "rule del"; |
197 most cases, one should have to change intro!! to intro? only); |
|
198 replaced "delrule" by "rule del"; |
198 |
199 |
199 * names of theorems etc. may be natural numbers as well; |
200 * names of theorems etc. may be natural numbers as well; |
200 |
201 |
201 * 'pr' command: optional arguments for goals_limit and |
202 * 'pr' command: optional arguments for goals_limit and |
202 ProofContext.prems_limit; no longer prints theory contexts, but only |
203 ProofContext.prems_limit; no longer prints theory contexts, but only |
333 * AddIffs now available, giving theorems of the form P<->Q to the |
334 * AddIffs now available, giving theorems of the form P<->Q to the |
334 simplifier and classical reasoner simultaneously; |
335 simplifier and classical reasoner simultaneously; |
335 |
336 |
336 |
337 |
337 *** General *** |
338 *** General *** |
|
339 |
|
340 * Provers: delrules now handles destruct rules as well (no longer need |
|
341 explicit make_elim); |
338 |
342 |
339 * Provers: blast(_tac) now handles actual object-logic rules as |
343 * Provers: blast(_tac) now handles actual object-logic rules as |
340 assumptions; note that auto(_tac) uses blast(_tac) internally as well; |
344 assumptions; note that auto(_tac) uses blast(_tac) internally as well; |
341 |
345 |
342 * Provers: Simplifier.easy_setup provides a fast path to basic |
346 * Provers: Simplifier.easy_setup provides a fast path to basic |