NEWS
changeset 5214 75c6392d1274
parent 5207 dd4f51adfff3
child 5217 3ecd7c952396
     1.1 --- a/NEWS	Thu Jul 30 15:49:18 1998 +0200
     1.2 +++ b/NEWS	Thu Jul 30 15:52:33 1998 +0200
     1.3 @@ -9,6 +9,25 @@
     1.4  
     1.5  * several changes of proof tools (see next section);
     1.6  
     1.7 +* HOL/datatype:
     1.8 +  - Theories using datatypes must now have Datatype.thy as an
     1.9 +    ancestor.
    1.10 +  - The specific <typename>.induct_tac no longer exists - use the
    1.11 +    generic induct_tac instead.
    1.12 +  - natE has been renamed to nat.exhaustion - use exhaust_tac
    1.13 +    instead of res_inst_tac ... natE. Note that the variable
    1.14 +    names in nat.exhaustion differ from the names in natE, this
    1.15 +    may cause some "fragile" proofs to fail.
    1.16 +  - the theorems split_<typename>_case and split_<typename>_case_asm
    1.17 +    have been renamed to <typename>.split and <typename>.split_asm.
    1.18 +  - Since default sorts are no longer ignored by the package,
    1.19 +    some datatype definitions may have to be annotated with
    1.20 +    explicit sort constraints.
    1.21 +  - Primrec definitions no longer require function name and type
    1.22 +    of recursive argument.
    1.23 +  Use isatool fixdatatype to adapt your theories and proof scripts
    1.24 +  to the new package (as usual, backup your sources first!).
    1.25 +
    1.26  * HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is
    1.27  now called `inj_on' (which makes more sense);
    1.28  
    1.29 @@ -93,6 +112,33 @@
    1.30  
    1.31  *** HOL ***
    1.32  
    1.33 +* HOL/datatype package reorganized and improved: now supports mutually
    1.34 +  recursive datatypes such as
    1.35 +
    1.36 +    datatype
    1.37 +      'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
    1.38 +              | SUM ('a aexp) ('a aexp)
    1.39 +              | DIFF ('a aexp) ('a aexp)
    1.40 +              | NUM 'a
    1.41 +    and
    1.42 +      'a bexp = LESS ('a aexp) ('a aexp)
    1.43 +              | AND ('a bexp) ('a bexp)
    1.44 +              | OR ('a bexp) ('a bexp)
    1.45 +
    1.46 +  as well as indirectly recursive datatypes such as
    1.47 +
    1.48 +    datatype
    1.49 +      ('a, 'b) term = Var 'a
    1.50 +                    | App 'b ((('a, 'b) term) list)
    1.51 +
    1.52 +  The new tactic
    1.53 +
    1.54 +    mutual_induct_tac [<var_1>, ..., <var_n>] i
    1.55 +
    1.56 +  performs induction on mutually / indirectly recursive datatypes.
    1.57 +  Primrec equations are now stored in theory and can be accessed
    1.58 +  via <function_name>.simps
    1.59 +
    1.60  * reorganized the main HOL image: HOL/Integ and String loaded by
    1.61  default; theory Main includes everything;
    1.62  
    1.63 @@ -123,7 +169,7 @@
    1.64  
    1.65    inductive EVEN ODD
    1.66      intrs
    1.67 -      null " 0 : EVEN"
    1.68 +      null "0 : EVEN"
    1.69        oddI "n : EVEN ==> Suc n : ODD"
    1.70        evenI "n : ODD ==> Suc n : EVEN"
    1.71