NEWS
2007-10-15 wenzelm 2007-10-15 more on authentic syntax;
2007-10-15 wenzelm 2007-10-15 updated method "ferrack";
2007-10-12 haftmann 2007-10-12 moved class power to theory Power
2007-10-12 haftmann 2007-10-12 class div inherits from class times
2007-10-10 wenzelm 2007-10-10 added 'no_notation';
2007-10-09 wenzelm 2007-10-09 tuned;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-07 wenzelm 2007-10-07 * Basic Isabelle mode for jEdit.
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-05 wenzelm 2007-10-05 tuned induct etc.;
2007-10-01 wenzelm 2007-10-01 added auto_quickcheck feature;
2007-10-01 wenzelm 2007-10-01 misc tuning and update;
2007-10-01 wenzelm 2007-10-01 misc tuning and update;
2007-09-26 wenzelm 2007-09-26 tuned;
2007-09-26 wenzelm 2007-09-26 tuned;
2007-09-26 wenzelm 2007-09-26 tuned;
2007-09-26 wenzelm 2007-09-26 * Pure/Isar: unified specification syntax admits type inference and dummy patterns; print mode: no_abbrevs;
2007-09-25 wenzelm 2007-09-25 * Pure/Syntax: generic interfaces for parsing and type checking; tuned;
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-24 wenzelm 2007-09-24 more ML antiqs;
2007-09-19 nipkow 2007-09-19 *** empty log message ***
2007-09-19 wenzelm 2007-09-19 * ML: just one true type int;
2007-09-18 ballarin 2007-09-18 Transitivity reasoner set up for locales.
2007-09-18 wenzelm 2007-09-18 moved Tools/integer.ML to Pure/General/integer.ML;
2007-09-18 nipkow 2007-09-18 *** empty log message ***
2007-09-16 wenzelm 2007-09-16 moved induct patterns to HOL/Induct/Common_Patterns.thy;
2007-09-01 nipkow 2007-09-01 *** empty log message ***
2007-08-31 wenzelm 2007-08-31 tuned multithreading entry -- no longer experimental;
2007-08-30 nipkow 2007-08-30 *** empty log message ***
2007-08-24 haftmann 2007-08-24 moved class dense_linear_order to Orderings.thy
2007-08-20 haftmann 2007-08-20 conciliated Inf/Inf_fin
2007-08-20 kleing 2007-08-20 * HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution
2007-08-13 kleing 2007-08-13 new attribute [rotated]
2007-08-12 wenzelm 2007-08-12 * Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
2007-08-10 wenzelm 2007-08-10 tuned; added jEdit mode spec;
2007-08-10 wenzelm 2007-08-10 * Experimental support for multithreading, using Poly/ML 5.1;
2007-08-08 wenzelm 2007-08-08 * Theory loader: old-style ML proof scripts are considered a legacy feature;
2007-08-07 wenzelm 2007-08-07 theory loader: added use_thys, removed obsolete update_thy; various global ML references of Pure and HOL have been turned into configuration options;
2007-08-01 wenzelm 2007-08-01 tuned config options: eliminated separate attribute "option";
2007-07-31 wenzelm 2007-07-31 * Configuration options; * Named collections of theorems;
2007-07-28 wenzelm 2007-07-28 * Isar: command 'declaration'; * Isar: proper interfaces for simplification procedures; * Isar: an extra pair of brackets around attribute declarations abbreviates a theorem reference involving an internal dummy fact;
2007-07-25 ballarin 2007-07-25 tuned
2007-07-24 krauss 2007-07-24 renamed lemma "set_take_whileD" to "set_takeWhileD"
2007-07-23 ballarin 2007-07-23 interpretation: unfolding of equations;
2007-07-20 wenzelm 2007-07-20 tuned;
2007-07-20 wenzelm 2007-07-20 * Theory loader: be more serious about observing the static theory header specifications; * Theory loader: optional support for content-based file identification;
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-07-19 haftmann 2007-07-19 updated
2007-07-11 berghofe 2007-07-11 Added entry for new inductive definition package.
2007-07-04 nipkow 2007-07-04 *** empty log message ***
2007-07-04 nipkow 2007-07-04 *** empty log message ***
2007-07-03 wenzelm 2007-07-03 tuned;
2007-06-27 nipkow 2007-06-27 *** empty log message ***
2007-06-25 obua 2007-06-25 commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-21 huffman 2007-06-21 changed simp rules for of_nat
2007-06-21 paulson 2007-06-21 integration of Metis prover
2007-06-14 wenzelm 2007-06-14 updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;