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

author | wenzelm |

Tue, 10 Jun 2008 19:15:14 +0200 | |

changeset 27122 | 63d92a5e3784 |

parent 27121 | 38367dbccae5 |

child 27123 | 11fcdd5897dd |

proper news header;
methods case_tac and induct_tac now refer to usual declarations;
removed obsolete induct_tac and thm_induct_tac;

--- a/NEWS Tue Jun 10 16:43:26 2008 +0200 +++ b/NEWS Tue Jun 10 19:15:14 2008 +0200 @@ -1,39 +1,46 @@ Isabelle NEWS -- history user-relevant changes ============================================== -New ---- +New in this Isabelle version +---------------------------- *** Pure *** -* 'instance': attached definitions now longer accepted. INCOMPATIBILITY. +* Command 'instance': attached definitions now longer accepted. +INCOMPATIBILITY. * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. *** HOL *** -* 'rep_datatype': instead of theorem names the command now takes a list of terms -denoting the constructors of the type to be represented as datatype. The -characteristic theorems have to be proven. INCOMPATIBILITY. Also observe that -the following theorems have disappeared in favour of existing ones: +* Methods "case_tac" and "induct_tac" now refer to the very same rule +declarations as the structured Isar versions "cases" and "induct", cf. +the corresponding "cases" and "induct" attributes. INCOMPATIBILITY, +in rare situations a different rule is selected --- notably nested +tuple elimination instead of former prod.exhaust: use explicit +(case_tac t rule: prod.exhaust) here. + +* Removed fact "case_split_thm", which duplicates "case_split". + +* Command 'rep_datatype': instead of theorem names the command now +takes a list of terms denoting the constructors of the type to be +represented as datatype. The characteristic theorems have to be +proven. INCOMPATIBILITY. Also observe that the following theorems +have disappeared in favour of existing ones: + unit_induct ~> unit.induct prod_induct ~> prod.induct sum_induct ~> sum.induct Suc_Suc_eq ~> nat.inject Suc_not_Zero Zero_not_Suc ~> nat.distinct -* Tactics induct_tac and thm_induct_tac now take explicit context as arguments; -type-specific induction rules are identified by the 'induct' attribute rather -than querying the datatype package directly. INCOMPATIBILITY. - * 'Least' operator now restricted to class 'order' (and subclasses). INCOMPATIBILITY. -* Library/Nat_Infinity: added addition, numeral syntax and more instantiations -for algebraic structures. Removed some duplicate theorems. Changes in simp -rules. INCOMPATIBILITY. - +* Library/Nat_Infinity: added addition, numeral syntax and more +instantiations for algebraic structures. Removed some duplicate +theorems. Changes in simp rules. INCOMPATIBILITY. New in Isabelle2008 (June 2008)