summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Thu, 30 Jul 1998 15:52:33 +0200 | |

changeset 5214 | 75c6392d1274 |

parent 5213 | 0aa62210e67c |

child 5215 | 3224d1a9a8f1 |

Adapted to new datatype package.

--- a/NEWS Thu Jul 30 15:49:18 1998 +0200 +++ b/NEWS Thu Jul 30 15:52:33 1998 +0200 @@ -9,6 +9,25 @@ * several changes of proof tools (see next section); +* HOL/datatype: + - Theories using datatypes must now have Datatype.thy as an + ancestor. + - The specific <typename>.induct_tac no longer exists - use the + generic induct_tac instead. + - natE has been renamed to nat.exhaustion - use exhaust_tac + instead of res_inst_tac ... natE. Note that the variable + names in nat.exhaustion differ from the names in natE, this + may cause some "fragile" proofs to fail. + - the theorems split_<typename>_case and split_<typename>_case_asm + have been renamed to <typename>.split and <typename>.split_asm. + - Since default sorts are no longer ignored by the package, + some datatype definitions may have to be annotated with + explicit sort constraints. + - Primrec definitions no longer require function name and type + of recursive argument. + Use isatool fixdatatype to adapt your theories and proof scripts + to the new package (as usual, backup your sources first!). + * HOL/inductive requires Inductive.thy as an ancestor; `inj_onto' is now called `inj_on' (which makes more sense); @@ -93,6 +112,33 @@ *** HOL *** +* HOL/datatype package reorganized and improved: now supports mutually + recursive datatypes such as + + datatype + 'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) + | SUM ('a aexp) ('a aexp) + | DIFF ('a aexp) ('a aexp) + | NUM 'a + and + 'a bexp = LESS ('a aexp) ('a aexp) + | AND ('a bexp) ('a bexp) + | OR ('a bexp) ('a bexp) + + as well as indirectly recursive datatypes such as + + datatype + ('a, 'b) term = Var 'a + | App 'b ((('a, 'b) term) list) + + The new tactic + + mutual_induct_tac [<var_1>, ..., <var_n>] i + + performs induction on mutually / indirectly recursive datatypes. + Primrec equations are now stored in theory and can be accessed + via <function_name>.simps + * reorganized the main HOL image: HOL/Integ and String loaded by default; theory Main includes everything; @@ -123,7 +169,7 @@ inductive EVEN ODD intrs - null " 0 : EVEN" + null "0 : EVEN" oddI "n : EVEN ==> Suc n : ODD" evenI "n : ODD ==> Suc n : EVEN"