NEWS
2007-11-20 wenzelm 2007-11-20 tuned spacing;
2007-11-15 wenzelm 2007-11-15 cover ISABELLE_IDENTIFIER;
2007-11-13 wenzelm 2007-11-13 tuned;
2007-11-12 schirmer 2007-11-12 fixed typo;
2007-11-11 wenzelm 2007-11-11 * HOL-Statespace;
2007-10-26 haftmann 2007-10-26 tuned
2007-10-26 krauss 2007-10-26 added NEWS entry for function package
2007-10-25 haftmann 2007-10-25 tuned
2007-10-24 wenzelm 2007-10-24 tuned file names etc.;
2007-10-24 haftmann 2007-10-24 tuned
2007-10-22 wenzelm 2007-10-22 tuned Nominal entry;
2007-10-22 wenzelm 2007-10-22 added @{sort}, @{type_syntax} antiquotations;
2007-10-21 wenzelm 2007-10-21 misc tuning;
2007-10-21 urbanc 2007-10-21 tuned the entry about nominal datatypes
2007-10-18 haftmann 2007-10-18 localized mono predicate
2007-10-16 haftmann 2007-10-16 global class syntax
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;