NEWS
2003-11-14 ballarin Type inference bug in Isar attributes "where" and "of" fixed.
2003-11-06 schirmer Records:
2003-11-06 ballarin Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
2003-10-22 paulson recursion
2003-10-16 paulson line-breaks; rewording
2003-10-15 kleing use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
2003-10-14 kleing allow \<^sub> in identifiers
2003-10-09 skalberg Added info on the new 'finalconsts' command.
2003-09-30 ballarin Improvements to Isar/Locales: premises generated by "includes" elements
2003-09-23 paulson new session HOL-SET-Protocol
2003-08-29 ballarin Method rule_tac understands Isar contexts: documentation.
2003-08-29 skalberg Removed the extended digits again.
2003-08-28 skalberg Fixed typos.
2003-08-27 skalberg Extended the notion of letter and digit, such that now one may use greek,
2003-07-29 kleing opened new section for next Isabelle release
2003-07-21 skalberg Added the specification command.
2003-05-12 ballarin Improved entry on Algebra.
2003-05-12 kleing MicroJava LBV
2003-05-12 schirmer Bali
2003-05-12 berghofe Program extraction framework.
2003-05-09 ballarin NEWS updated for HOL-Algebra.
2003-05-06 paulson removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
2003-05-05 paulson Complex, etc
2003-05-05 kleing fixed \<0>..\<9> (-> \<zero>..\<nine>)
2003-05-05 kleing document preparation tuning
2003-04-30 ballarin Simplifier: congruence rule update.
2003-04-06 nipkow *** empty log message ***
2003-03-25 berghofe Presburger arithmetic
2003-03-20 paulson Gauss, UNITY, ZF
2003-03-18 nipkow *** empty log message ***
2003-02-27 ballarin Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-25 nipkow *** empty log message ***
2003-02-20 paulson minor updates to pre-2002 release
2003-02-11 nipkow *** empty log message ***
2003-01-17 nipkow *** empty log message ***
2002-12-11 ballarin HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
2002-11-28 ballarin HOL-Algebra partially ported to Isar.
2002-10-14 nipkow *** empty log message ***
2002-10-10 nipkow *** empty log message ***
2002-10-10 nipkow *** empty log message ***
2002-10-01 berghofe Added some comments on new simplifier.
2002-09-30 nipkow *** empty log message ***
2002-09-26 paulson GroupTheory and FuncSet
2002-09-19 nipkow *** empty log message ***
2002-08-30 paulson removal of blast.overloaded
2002-08-29 wenzelm updated;
2002-08-27 wenzelm *** empty log message ***
2002-08-27 wenzelm * Pure: disallow duplicate fact bindings within new-style theory files;
2002-08-27 wenzelm * Isar: preview of problems to finish 'show' now produce an error
2002-08-23 nipkow *** empty log message ***
2002-08-13 nipkow *** empty log message ***
2002-08-12 nipkow *** empty log message ***
2002-08-08 wenzelm * Pure: improved error reporting of simprocs;
2002-08-06 wenzelm * Provers: Simplifier.simproc(_i) now provide sane interface for
2002-08-06 wenzelm * Pure: predefined locales "var" and "struct" are useful for sharing
2002-08-02 wenzelm typedef: "open" option;
2002-07-26 wenzelm support for split assumptions in cases (hyps vs. prems);
2002-07-23 wenzelm * Pure: locale specifications now produce predicate definitions;
2002-07-11 nipkow *** empty log message ***
2002-07-02 wenzelm thms_containing: optional limit argument;
less more (0) -300 -100 -60 tip