NEWS
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type vars.
2003-12-06 kleing 2003-12-06 moreover and also do not reset facts any more
2003-11-14 ballarin 2003-11-14 Type inference bug in Isar attributes "where" and "of" fixed.
2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-11-06 ballarin 2003-11-06 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.
2003-10-22 paulson 2003-10-22 recursion
2003-10-16 paulson 2003-10-16 line-breaks; rewording
2003-10-15 kleing 2003-10-15 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
2003-10-15 kleing 2003-10-15 allow \<^sub> in identifiers
2003-10-09 skalberg 2003-10-09 Added info on the new 'finalconsts' command.
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
2003-09-23 paulson 2003-09-23 new session HOL-SET-Protocol
2003-08-29 ballarin 2003-08-29 Method rule_tac understands Isar contexts: documentation.
2003-08-29 skalberg 2003-08-29 Removed the extended digits again.
2003-08-28 skalberg 2003-08-28 Fixed typos.
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2003-07-29 kleing 2003-07-29 opened new section for next Isabelle release
2003-07-21 skalberg 2003-07-21 Added the specification command.
2003-05-12 ballarin 2003-05-12 Improved entry on Algebra.
2003-05-12 kleing 2003-05-12 MicroJava LBV
2003-05-12 schirmer 2003-05-12 Bali
2003-05-12 berghofe 2003-05-12 Program extraction framework.
2003-05-09 ballarin 2003-05-09 NEWS updated for HOL-Algebra.
2003-05-06 paulson 2003-05-06 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
2003-05-05 paulson 2003-05-05 Complex, etc
2003-05-05 kleing 2003-05-05 fixed \<0>..\<9> (-> \<zero>..\<nine>)
2003-05-05 kleing 2003-05-05 document preparation tuning
2003-04-30 ballarin 2003-04-30 Simplifier: congruence rule update.
2003-04-06 nipkow 2003-04-06 *** empty log message ***
2003-03-25 berghofe 2003-03-25 Presburger arithmetic
2003-03-20 paulson 2003-03-20 Gauss, UNITY, ZF
2003-03-18 nipkow 2003-03-18 *** empty log message ***
2003-02-27 ballarin 2003-02-27 Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-25 nipkow 2003-02-25 *** empty log message ***
2003-02-20 paulson 2003-02-20 minor updates to pre-2002 release
2003-02-11 nipkow 2003-02-11 *** empty log message ***
2003-01-17 nipkow 2003-01-17 *** empty log message ***
2002-12-11 ballarin 2002-12-11 HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2002-10-14 nipkow 2002-10-14 *** empty log message ***
2002-10-10 nipkow 2002-10-10 *** empty log message ***
2002-10-10 nipkow 2002-10-10 *** empty log message ***
2002-10-01 berghofe 2002-10-01 Added some comments on new simplifier.
2002-09-30 nipkow 2002-09-30 *** empty log message ***
2002-09-26 paulson 2002-09-26 GroupTheory and FuncSet
2002-09-19 nipkow 2002-09-19 *** empty log message ***
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-08-29 wenzelm 2002-08-29 updated;
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-27 wenzelm 2002-08-27 * Pure: disallow duplicate fact bindings within new-style theory files;
2002-08-27 wenzelm 2002-08-27 * Isar: preview of problems to finish 'show' now produce an error
2002-08-23 nipkow 2002-08-23 *** empty log message ***
2002-08-13 nipkow 2002-08-13 *** empty log message ***
2002-08-12 nipkow 2002-08-12 *** empty log message ***
2002-08-08 wenzelm 2002-08-08 * Pure: improved error reporting of simprocs; tuned;
2002-08-06 wenzelm 2002-08-06 * Provers: Simplifier.simproc(_i) now provide sane interface for setting up simprocs;
2002-08-06 wenzelm 2002-08-06 * Pure: predefined locales "var" and "struct" are useful for sharing parameters (as in CASL, for example); just specify something like ``var x + var y + struct M'' as import;
2002-08-02 wenzelm 2002-08-02 typedef: "open" option;
2002-07-26 wenzelm 2002-07-26 support for split assumptions in cases (hyps vs. prems);
2002-07-24 wenzelm 2002-07-24 * Pure: locale specifications now produce predicate definitions;