summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 9612 | e6ba17cd012e |

parent 9577 | 9e66e8ed8237 |

child 9647 | e9623f47275b |

1.1 --- a/NEWS Wed Aug 16 18:10:15 2000 +0200 1.2 +++ b/NEWS Thu Aug 17 10:29:23 2000 +0200 1.3 @@ -54,6 +54,10 @@ 1.4 1.5 * Isar: changed syntax of local blocks from {{ }} to { }; 1.6 1.7 +* Isar: renamed 'RS' attribute to 'THEN'; 1.8 + 1.9 +* Isar/HOL: renamed "intrs" to "intros" in inductive definitions; 1.10 + 1.11 * Provers: strengthened force_tac by using new first_best_tac; 1.12 1.13 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. 1.14 @@ -130,12 +134,14 @@ 1.15 1.16 * Pure: changed syntax of local blocks from {{ }} to { }; 1.17 1.18 +* Pure: renamed 'RS' attribute to 'THEN'; 1.19 + 1.20 * Pure: syntax of sorts made 'inner', i.e. have to write "{a, b, c}" 1.21 instead of {a, b, c}; 1.22 1.23 * Pure now provides its own version of intro/elim/dest attributes; 1.24 useful for building new logics, but beware of confusion with the 1.25 -Provers/classical ones; 1.26 +version in Provers/classical; 1.27 1.28 * Pure: the local context of (non-atomic) goals is provided via case 1.29 name 'antecedent'; 1.30 @@ -146,10 +152,18 @@ 1.31 * Pure: theory command 'method_setup' provides a simple interface for 1.32 definining proof methods in ML; 1.33 1.34 +* Provers: hypsubst support; also plain subst and symmetric attribute 1.35 +(the latter supercedes [RS sym]); 1.36 + 1.37 * Provers: splitter support (via 'split' attribute and 'simp' method 1.38 modifier); 'simp' method: 'only:' modifier removes loopers as well 1.39 (including splits); 1.40 1.41 +* Provers: added 'fastsimp' and 'clarsimp' methods (combination of 1.42 +Simplifier and Classical reasoner); 1.43 + 1.44 +* Provers: added 'arith_split' attribute; 1.45 + 1.46 * HOL: new proof method 'cases' and improved version of 'induct' now 1.47 support named cases; major packages (inductive, datatype, primrec, 1.48 recdef) support case names and properly name parameters; 1.49 @@ -157,19 +171,24 @@ 1.50 * HOL: removed 'case_split' thm binding, should use 'cases' proof 1.51 method anyway; 1.52 1.53 -* HOL/Calculation: new rules for substitution in inequalities 1.54 -(monotonicity conditions are extracted to be proven at end); 1.55 - 1.56 * HOL: removed obsolete expand_if = split_if; theorems if_splits = 1.57 split_if split_if_asm; datatype package provides theorems foo.splits = 1.58 foo.split foo.split_asm for each datatype; 1.59 1.60 -* names of theorems etc. may be natural numbers as well; 1.61 +* HOL/Calculation: new rules for substitution in inequalities 1.62 +(monotonicity conditions are extracted to be proven at end); 1.63 + 1.64 +* HOL/inductive: rename "intrs" to "intros" (potential 1.65 +INCOMPATIBILITY); emulation of mk_cases feature for proof scripts: 1.66 +'inductive_cases' command and 'ind_cases' method; NOTE: use (cases 1.67 +(simplified)) method in proper proofs; 1.68 1.69 * Provers: intro/elim/dest attributes: changed intro/intro!/intro!! 1.70 flags to intro!/intro/intro? (in most cases, one should have to change 1.71 intro!! to intro? only); 1.72 1.73 +* names of theorems etc. may be natural numbers as well; 1.74 + 1.75 * 'pr' command: optional goals_limit argument; no longer prints theory 1.76 contexts, but only proof states; 1.77 1.78 @@ -178,8 +197,9 @@ 1.79 proof state according to the Isabelle LaTeX style; 1.80 1.81 * improved support for emulating tactic scripts, including proof 1.82 -methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' / 1.83 -'induct_tac' (for HOL datatypes); 1.84 +methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac', 1.85 +'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac' 1.86 +(for HOL datatypes); 1.87 1.88 * simplified (more robust) goal selection of proof methods: 1st goal, 1.89 all goals, or explicit goal specifier (tactic emulation); thus 'proof 1.90 @@ -213,8 +233,9 @@ 1.91 1.92 * HOL/Real: "rabs" replaced by overloaded "abs" function; 1.93 1.94 -* HOL/record: fixed select-update simplification procedure to handle 1.95 -extended records as well; admit "r" as field name; 1.96 +* HOL/record: added general record equality rule to simpset; fixed 1.97 +select-update simplification procedure to handle extended records as 1.98 +well; admit "r" as field name; 1.99 1.100 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with 1.101 other numeric types and also as the identity of groups, rings, etc.; 1.102 @@ -379,11 +400,11 @@ 1.103 reasoning); for further information see isatool doc isar-ref, 1.104 src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/ 1.105 1.106 -* improved presentation of theories: better HTML markup (including 1.107 -colors), graph views in several sizes; isatool usedir now provides a 1.108 -proper interface for user theories (via -P option); actual document 1.109 -preparation based on (PDF)LaTeX is available as well (for new-style 1.110 -theories only); see isatool doc system for more information; 1.111 +* improved and simplified presentation of theories: better HTML markup 1.112 +(including colors), graph views in several sizes; isatool usedir now 1.113 +provides a proper interface for user theories (via -P option); actual 1.114 +document preparation based on (PDF)LaTeX is available as well (for 1.115 +new-style theories only); see isatool doc system for more information; 1.116 1.117 * native support for Proof General, both for classic Isabelle and 1.118 Isabelle/Isar;