2009-03-27 ago merged
2009-03-27 ago dropped toy example Code_Antiq
2009-03-26 ago interpretation/interpret: prefixes are mandatory by default;
2009-03-24 ago NEWS: [arith]
2009-03-20 ago Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-19 ago tuned;
2009-03-16 ago document new additions to HOL/Library
2009-03-16 ago simplifief 'method_setup' command;
2009-03-15 ago merged
2009-03-14 ago updated NEWS
2009-03-15 ago simplified attribute and method setup;
2009-03-11 ago added 'local_setup' command;
2009-03-11 ago Updated paths in Decision_Procs comments and NEWS
2009-03-10 ago Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2009-03-09 ago tuned;
2009-03-09 ago * More systematic treatment of long names, abstract name bindings, and name space operations.
2009-03-06 ago constructive version of Cantor's first diagonalization argument
2009-03-06 ago merged
2009-03-05 ago merged
2009-03-05 ago set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-06 ago corrected slip in NEWS
2009-03-06 ago added strict_mono predicate
2009-03-04 ago declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 ago NEWS: renamed o2s to Option.set;
2009-03-04 ago Made Option a separate theory and renamed option_map to
2009-03-03 ago removed and renamed redundant lemmas
2009-03-02 ago name fix
2009-03-02 ago name changes
2009-03-01 ago removed redundant lemmas
2009-02-28 ago add news for HOLCF; fixed some typos and inaccuracies
2009-02-28 ago * New prover for coherent logic (see src/Tools/coherent.ML).
2009-02-26 ago tuned NEWS;
2009-02-25 ago NEWS
2009-02-21 ago NEWS
2009-02-13 ago added find_consts to NEWS and CONTRIBUTORS
2009-02-11 ago fixed typo
2009-02-11 ago updated NEWS etc with "solves" criterion and auto_solves
2009-02-06 ago session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-05 ago Updated NEWS about approximation
2009-02-05 ago Add approximation method
2009-02-03 ago handling type classes without parameters
2009-02-03 ago established session HOL-Reflection
2009-01-28 ago -
2009-01-28 ago Reflection.thy now in HOL/Library
2009-01-26 ago entry point for Word library now named Word
2009-01-22 ago binding replaces Binding.T
2009-01-21 ago no base sort in class import
2009-01-08 ago NEWS and CONTRIBUTORS
2008-12-30 ago New locales.
2008-12-29 ago adapted HOL source structure to distribution layout
2008-12-27 ago tuned NEWS; CONTRIBUTORS
2008-12-23 ago tuned;
2008-12-23 ago * Proofs of are run in parallel on multi-core systems;
2008-12-20 ago removed Ids;
2008-12-16 ago method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-12-04 ago merged
2008-12-04 ago cleaned up binding module and related code
2008-12-04 ago NEWS
2008-12-03 ago made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-11-30 ago removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;