Adapted to new inductive definition package.
authorberghofe
Wed Jul 01 19:11:20 1998 +0200 (1998-07-01)
changeset 5109b3d18eb3ac20
parent 5108 4074c7d86d44
child 5110 2497807020fa
Adapted to new inductive definition package.
NEWS
     1.1 --- a/NEWS	Wed Jul 01 19:03:54 1998 +0200
     1.2 +++ b/NEWS	Wed Jul 01 19:11:20 1998 +0200
     1.3 @@ -46,6 +46,20 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Inductive definition package: Mutually recursive definitions such as
     1.8 +
     1.9 +  inductive EVEN ODD
    1.10 +    intrs
    1.11 +      null " 0 : EVEN"
    1.12 +      oddI "n : EVEN ==> Suc n : ODD"
    1.13 +      evenI "n : ODD ==> Suc n : EVEN"
    1.14 +
    1.15 +  are now possible. Theories containing (co)inductive definitions must now
    1.16 +  have theory "Inductive" as an ancestor. The new component "elims" of the
    1.17 +  structure created by the package contains an elimination rule for each of
    1.18 +  the recursive sets. Note that the component "mutual_induct" no longer
    1.19 +  exists - the induction rule is always contained in "induct".
    1.20 +
    1.21  * HOL/Real: a construction of the reals using Dedekind cuts
    1.22  
    1.23  * HOL/record: now includes concrete syntax for record terms (still