tuned;
authorwenzelm
Sat Nov 24 16:53:31 2001 +0100 (2001-11-24)
changeset 12280fc7e3f01bc40
parent 12279 dc3020e938e2
child 12281 3bd113b8f7a6
tuned;
NEWS
     1.1 --- a/NEWS	Sat Nov 24 13:58:19 2001 +0100
     1.2 +++ b/NEWS	Sat Nov 24 16:53:31 2001 +0100
     1.3 @@ -33,39 +33,33 @@
     1.4  *** Isar ***
     1.5  
     1.6  * improved proof by cases and induction:
     1.7 +  - 'case' command admits impromptu naming of parameters (such as
     1.8 +    "case (Suc n)");
     1.9 +  - 'induct' method divinates rule instantiation from the inductive
    1.10 +    claim; no longer requires excessive ?P bindings for proper
    1.11 +    instantiation of cases;
    1.12 +  - 'induct' method properly enumerates all possibilities of set/type
    1.13 +    rules; as a consequence facts may be also passed through *type*
    1.14 +    rules without further ado;
    1.15 +  - 'induct' method now derives symbolic cases from the *rulified*
    1.16 +    rule (before it used to rulify cases stemming from the internal
    1.17 +    atomized version); this means that the context of a non-atomic
    1.18 +    statement becomes is included in the hypothesis, avoiding the
    1.19 +    slightly cumbersome show "PROP ?case" form;
    1.20 +  - 'induct' may now use elim-style induction rules without chaining
    1.21 +    facts, using ``missing'' premises from the goal state; this allows
    1.22 +    rules stemming from inductive sets to be applied in unstructured
    1.23 +    scripts, while still benefitting from proper handling of non-atomic
    1.24 +    statements; NB: major inductive premises need to be put first, all
    1.25 +    the rest of the goal is passed through the induction;
    1.26 +  - 'induct' proper support for mutual induction involving non-atomic
    1.27 +    rule statements (uses the new concept of simultaneous goals, see
    1.28 +    below);
    1.29    - removed obsolete "(simplified)" and "(stripped)" options of methods;
    1.30    - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
    1.31    - moved induct/cases attributes to Pure, methods to Provers;
    1.32    - generic method setup instantiated for FOL and HOL;
    1.33  
    1.34 -  - 'case' command admits impromptu naming of parameters (such as
    1.35 -"case (Suc n)");
    1.36 -
    1.37 -  - 'induct' method divinates rule instantiation from the inductive
    1.38 -claim; no longer requires excessive ?P bindings for proper
    1.39 -instantiation of cases;
    1.40 -
    1.41 -  - 'induct' method properly enumerates all possibilities of set/type
    1.42 -rules; as a consequence facts may be also passed through *type* rules
    1.43 -without further ado;
    1.44 -
    1.45 -  - 'induct' method now derives symbolic cases from the *rulified*
    1.46 -rule (before it used to rulify cases stemming from the internal
    1.47 -atomized version); this means that the context of a non-atomic
    1.48 -statement becomes is included in the hypothesis, avoiding the slightly
    1.49 -cumbersome show "PROP ?case" form;
    1.50 -
    1.51 -  - 'induct' may now use elim-style induction rules without chaining
    1.52 -facts, using ``missing'' premises from the goal state; this allows
    1.53 -rules stemming from inductive sets to be applied in unstructured
    1.54 -scripts, while still benefitting from proper handling of non-atomic
    1.55 -statements; NB: major inductive premises need to be put first, all the
    1.56 -rest of the goal is passed through the induction;
    1.57 -
    1.58 -- 'induct' proper support for mutual induction involving non-atomic
    1.59 -rule statements (uses the new concept of simultaneous goals, see
    1.60 -below);
    1.61 -
    1.62  * Pure: support multiple simultaneous goal statements, for example
    1.63  "have a: A and b: B" (same for 'theorem' etc.); being a pure
    1.64  meta-level mechanism, this acts as if several individual goals had
    1.65 @@ -82,7 +76,8 @@
    1.66  * Pure: proper integration with ``locales''; unlike the original
    1.67  version by Florian Kammüller, Isar locales package high-level proof
    1.68  contexts rather than raw logical ones (e.g. we admit to include
    1.69 -attributes everywhere);
    1.70 +attributes everywhere); operations on locales include merge and
    1.71 +rename; e.g. see HOL/ex/Locales.thy;
    1.72  
    1.73  * Pure: theory goals now support ad-hoc contexts, which are discharged
    1.74  in the result, as in ``lemma (assumes A and B) K: A .''; syntax
    1.75 @@ -122,6 +117,14 @@
    1.76  * HOL: 'inductive' no longer features separate (collective) attributes
    1.77  for 'intros' (was found too confusing);
    1.78  
    1.79 +* HOLCF: domain package adapted to new-style theories, e.g. see
    1.80 +HOLCF/ex/Dnat.thy;
    1.81 +
    1.82 +* ZF: proper integration of logic-specific tools and packages,
    1.83 +including theory commands '(co)inductive', '(co)datatype',
    1.84 +'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',
    1.85 +'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
    1.86 +
    1.87  
    1.88  
    1.89  *** HOL ***
    1.90 @@ -152,16 +155,17 @@
    1.91  
    1.92    - remove all special provisions on numerals in proofs;
    1.93  
    1.94 -* HOL/record:
    1.95 -  - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;
    1.96 +* HOL/record package improvements:
    1.97 +  - new derived operations "fields" to build a partial record section,
    1.98 +    "extend" to promote a fixed record to a record scheme, and
    1.99 +    "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*
   1.100 +    declared as simp by default;
   1.101 +  - removed "make_scheme" operations (use "make" with "extend") --
   1.102 +    INCOMPATIBILITY;
   1.103    - removed "more" class (simply use "term") -- INCOMPATIBILITY;
   1.104    - provides cases/induct rules for use with corresponding Isar
   1.105      methods (for concrete records, record schemes, concrete more
   1.106 -    parts, schematic more parts -- in that order);
   1.107 -  - new derived operations "make" (for adding fields of current
   1.108 -    record), "extend" to promote fixed record to record scheme, and
   1.109 -    "truncate" for the reverse; cf. theorems "derived_defs", which are
   1.110 -    *not* declared as simp by default;
   1.111 +    parts, and schematic more parts -- in that order);
   1.112    - internal definitions directly based on a light-weight abstract
   1.113      theory of product types over typedef rather than datatype;
   1.114  
   1.115 @@ -202,61 +206,62 @@
   1.116  
   1.117  *** HOLCF ***
   1.118  
   1.119 -* proper rep_datatype lift (see theory Lift); use plain induct_tac
   1.120 -instead of former lift.induct_tac; always use UU instead of Undef;
   1.121 -
   1.122 -* 'domain' package adapted to new-style theories, e.g. see
   1.123 -HOLCF/ex/Dnat.thy;
   1.124 +* proper rep_datatype lift (see theory Lift) instead of ML hacks --
   1.125 +potential INCOMPATIBILITY; now use plain induct_tac instead of former
   1.126 +lift.induct_tac, always use UU instead of Undef;
   1.127  
   1.128  
   1.129  *** ZF ***
   1.130  
   1.131 -* ZF: new-style theory commands '(co)inductive', '(co)datatype',
   1.132 -'rep_datatype', 'inductive_cases'; also methods 'ind_cases',
   1.133 -'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
   1.134 +* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
   1.135 +typeless version of the formalism;
   1.136 +
   1.137 +* ZF/Induct: new directory for examples of inductive definitions,
   1.138 +including theory Multiset for multiset orderings;
   1.139  
   1.140  * ZF: the integer library now covers quotients and remainders, with
   1.141  many laws relating division to addition, multiplication, etc.;
   1.142  
   1.143 -* ZF/Induct: new directory for examples of inductive definitions,
   1.144 -including theory Multiset for multiset orderings;
   1.145 -
   1.146 -* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
   1.147 -typeless version of the formalism;
   1.148 -
   1.149  
   1.150  *** General ***
   1.151  
   1.152 -* kernel: meta-level proof terms (by Stefan Berghofer), see also ref
   1.153 -manual;
   1.154 -
   1.155 -* Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;
   1.156 -
   1.157 -* classical: renamed addaltern to addafter, addSaltern to addSafter;
   1.158 -
   1.159 -* clasimp: ``iff'' declarations now handle conditional rules as well;
   1.160 -
   1.161 -* syntax: new token syntax "num" for plain numerals (without "#" of
   1.162 -"xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now separate
   1.163 -tokens, so expressions involving minus need to be spaced properly;
   1.164 -
   1.165 -* syntax: support non-oriented infixes;
   1.166 -
   1.167 -* syntax: print modes "type_brackets" and "no_type_brackets" control
   1.168 -output of nested => (types); the default behavior is "type_brackets";
   1.169 -
   1.170 -* syntax: builtin parse translation for "_constify" turns valued
   1.171 +* Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference
   1.172 +variable proof controls level of detail: 0 = no proofs (only oracle
   1.173 +dependencies), 1 = lemma dependencies, 2 = compact proof terms; see
   1.174 +also ref manual for further ML interfaces;
   1.175 +
   1.176 +* Pure/axclass: removed obsolete ML interface
   1.177 +goal_subclass/goal_arity;
   1.178 +
   1.179 +* Pure/syntax: new token syntax "num" for plain numerals (without "#"
   1.180 +of "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now
   1.181 +separate tokens, so expressions involving minus need to be spaced
   1.182 +properly;
   1.183 +
   1.184 +* Pure/syntax: support non-oriented infixes;
   1.185 +
   1.186 +* Pure/syntax: print modes "type_brackets" and "no_type_brackets"
   1.187 +control output of nested => (types); the default behavior is
   1.188 +"type_brackets";
   1.189 +
   1.190 +* Pure/syntax: builtin parse translation for "_constify" turns valued
   1.191  tokens into AST constants;
   1.192  
   1.193 -* syntax: prefer later print_translation functions; potential
   1.194 -INCOMPATIBILITY: need to reverse declarations of multiple translation
   1.195 -functions for same constant;
   1.196 +* Pure/syntax: prefer later declarations of translations and print
   1.197 +translation functions; potential INCOMPATIBILITY: need to reverse
   1.198 +multiple declarations for same syntax element constant;
   1.199 +
   1.200 +* Provers/classical: renamed addaltern to addafter, addSaltern to
   1.201 +addSafter;
   1.202 +
   1.203 +* Provers/clasimp: ``iff'' declarations now handle conditional rules
   1.204 +as well;
   1.205  
   1.206  * system: refrain from any attempt at filtering input streams; no
   1.207  longer support ``8bit'' encoding of old isabelle font, instead proper
   1.208  iso-latin characters may now be used;
   1.209  
   1.210 -* system: support Poly/ML 4.1.1 (now able to manage large heaps);
   1.211 +* system: support Poly/ML 4.1.1 (able to manage larger heaps);
   1.212  
   1.213  * system: Proof General keywords specification is now part of the
   1.214  Isabelle distribution (see etc/isar-keywords.el);