NEWS
changeset 8729 094dbd0fad0c
parent 8705 a3da5538d924
child 8736 0bfd6678a5fa
equal deleted inserted replaced
8728:33a9643ba626 8729:094dbd0fad0c
       
     1 
     1 Isabelle NEWS -- history user-relevant changes
     2 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     3 ==============================================
     3 
     4 
     4 New in this Isabelle version
     5 New in this Isabelle version
     5 ----------------------------
     6 ----------------------------
     6 
     7 
     7 *** Overview of INCOMPATIBILITIES (see below for more details) ***
     8 *** Overview of INCOMPATIBILITIES (see below for more details) ***
     8 
     9 
     9 * HOL: the constant for f``x is now "image" rather than "op ``".
    10 * HOL: the constant for f``x is now "image" rather than "op ``";
    10 
    11 
    11 * HOL: the cartesian product is now "<*>" instead of "Times".
    12 * HOL: the cartesian product is now "<*>" instead of "Times"; the
    12        the lexicographic product is now "<*lex*>" instead of "**".
    13 lexicographic product is now "<*lex*>" instead of "**";
    13 
    14 
    14 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
    15 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
    15 
    16 
    16 * HOL: simplification no longer dives into case-expressions
    17 * HOL: simplification no longer dives into case-expressions
    17 
    18 
    18 * HOL: the recursion equations generated by 'recdef' are now called
    19 * HOL: the recursion equations generated by 'recdef' are now called
    19 f.simps instead of f.rules;
    20 f.simps instead of f.rules;
    20 
    21 
    21 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    22 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
       
    23 
       
    24 * LaTeX: several improvements of isabelle.sty;
    22 
    25 
    23 
    26 
    24 *** Document preparation ***
    27 *** Document preparation ***
    25 
    28 
    26 * isatool mkdir provides easy setup of Isabelle session directories,
    29 * isatool mkdir provides easy setup of Isabelle session directories,
    85 * simplified (more robust) goal selection of proof methods: 1st goal,
    88 * simplified (more robust) goal selection of proof methods: 1st goal,
    86 all goals, or explicit goal specifier (tactic emulation); thus 'proof
    89 all goals, or explicit goal specifier (tactic emulation); thus 'proof
    87 method scripts' have to be in depth-first order;
    90 method scripts' have to be in depth-first order;
    88 
    91 
    89 * tuned 'let' syntax: replace 'as' keyword by 'and';
    92 * tuned 'let' syntax: replace 'as' keyword by 'and';
       
    93 
       
    94 * theory command 'hide' removes declarations from class/type/const
       
    95 name spaces;
    90 
    96 
    91 
    97 
    92 *** HOL ***
    98 *** HOL ***
    93 
    99 
    94 * HOL/Algebra: new theory of rings and univariate polynomials, by
   100 * HOL/Algebra: new theory of rings and univariate polynomials, by
   121 resulting in a separate list of theorems for each equation;
   127 resulting in a separate list of theorems for each equation;
   122 
   128 
   123 
   129 
   124 *** General ***
   130 *** General ***
   125 
   131 
       
   132 * improved name spaces: ambiguous output is qualified; support for
       
   133 hiding of names;
       
   134 
   126 * compression of ML heaps images may now be controlled via -c option
   135 * compression of ML heaps images may now be controlled via -c option
   127 of isabelle and isatool usedir (currently only observed by Poly/ML);
   136 of isabelle and isatool usedir (currently only observed by Poly/ML);
   128 
   137 
   129 * ML: new combinators |>> and |>>> for incremental transformations
   138 * ML: new combinators |>> and |>>> for incremental transformations
   130 with secondary results (e.g. certain theory extensions):
   139 with secondary results (e.g. certain theory extensions):
   161 uses the default simpset instead of a supplied list of theorems.
   170 uses the default simpset instead of a supplied list of theorems.
   162 
   171 
   163 * HOL/List: the constructors of type list are now Nil and Cons;
   172 * HOL/List: the constructors of type list are now Nil and Cons;
   164 
   173 
   165 * Simplifier: the type of the infix ML functions
   174 * Simplifier: the type of the infix ML functions
   166 	setSSolver addSSolver setSolver addSolver
   175         setSSolver addSSolver setSolver addSolver
   167 is now  simpset * solver -> simpset  where `solver' is a new abstract type
   176 is now  simpset * solver -> simpset  where `solver' is a new abstract type
   168 for packaging solvers. A solver is created via
   177 for packaging solvers. A solver is created via
   169 	mk_solver: string -> (thm list -> int -> tactic) -> solver
   178         mk_solver: string -> (thm list -> int -> tactic) -> solver
   170 where the string argument is only a comment.
   179 where the string argument is only a comment.
   171 
   180 
   172 
   181 
   173 *** Proof tools ***
   182 *** Proof tools ***
   174 
   183 
   384 * the notation <<...>> is now available as a notation for sequences of
   393 * the notation <<...>> is now available as a notation for sequences of
   385 formulas;
   394 formulas;
   386 
   395 
   387 * the simplifier is now installed
   396 * the simplifier is now installed
   388 
   397 
   389 * the axiom system has been generalized (thanks to Soren Heilmann) 
   398 * the axiom system has been generalized (thanks to Soren Heilmann)
   390 
   399 
   391 * the classical reasoner now has a default rule database
   400 * the classical reasoner now has a default rule database
   392 
   401 
   393 
   402 
   394 *** ZF ***
   403 *** ZF ***