author | berghofe |

Wed Jul 01 19:11:20 1998 +0200 (1998-07-01) | |

changeset 5109 | b3d18eb3ac20 |

parent 5108 | 4074c7d86d44 |

child 5110 | 2497807020fa |

Adapted to new inductive definition package.

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