2011-01-07 bulwahn 2011-01-07 merged
2011-01-07 bulwahn 2011-01-07 removing obselete Id comments from HOL/ex theories
2011-01-07 boehmes 2011-01-07 added hints about licensing restrictions and how to enable Z3
2011-01-07 boehmes 2011-01-07 tuned
2011-01-07 wenzelm 2011-01-07 eliminated hard tabs;
2011-01-07 wenzelm 2011-01-07 allow spaces in $SPASS_HOME value;
2011-01-07 wenzelm 2011-01-07 tuned;
2011-01-07 wenzelm 2011-01-07 eliminated alias;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2011-01-07 wenzelm 2011-01-07 more standard package setup;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2011-01-07 wenzelm 2011-01-07 updated scala; removed jedit -- component needs to be build afresh from ISABELLE_HOME/src/Tools/jEdit;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2011-01-07 wenzelm 2011-01-07 do not open Codegen;
2011-01-07 wenzelm 2011-01-07 tuned whitespace, indentation, comments;
2011-01-07 wenzelm 2011-01-07 updated for release;
2011-01-07 wenzelm 2011-01-07 tuned;
2011-01-07 wenzelm 2011-01-07 more precise parentheses and indentation; eliminated trailing whitespace;
2011-01-07 wenzelm 2011-01-07 comments;
2011-01-07 wenzelm 2011-01-07 updated for 2011; emphasize "contributors" in the header as well, which are already mentioned in the body text;
2011-01-07 boehmes 2011-01-07 shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
2011-01-07 krauss 2011-01-07 tuned NEWS
2011-01-07 boehmes 2011-01-07 avoid ML structure aliases (especially single-letter abbreviations)
2011-01-07 boehmes 2011-01-07 made SML/NJ happy
2011-01-06 huffman 2011-01-06 rename constant u_defl to u_liftdefl; add new constant u_defl :: udom defl -> udom defl
2011-01-06 huffman 2011-01-06 rename constant pdefl to liftdefl_of
2011-01-06 ballarin 2011-01-06 Diagnostic command to show locale dependencies.
2011-01-06 ballarin 2011-01-06 Documentation for 'interpret' and 'sublocale' with mixins.
2011-01-06 ballarin 2011-01-06 Abelian group facts obtained from group facts via interpretation (sublocale).
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
2011-01-04 huffman 2011-01-04 remove various lemmas redundant with lub_eq_bottom_iff
2011-01-04 huffman 2011-01-04 change some lemma names containing 'UU' to 'bottom'
2011-01-04 huffman 2011-01-04 renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax; removed redundant lemma UU_least
2011-01-03 boehmes 2011-01-03 merged
2011-01-03 boehmes 2011-01-03 updated SMT certificates
2011-01-03 boehmes 2011-01-03 re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs
2011-01-03 haftmann 2011-01-03 tuned whitespace
2010-12-31 wenzelm 2010-12-31 do not open structure Codegen;
2010-12-30 wenzelm 2010-12-30 do not open auxiliary ML structures;
2010-12-30 wenzelm 2010-12-30 uniform treatment of type vs. term environment (cf. b654fa27fbc4); tuned;
2010-12-30 wenzelm 2010-12-30 uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
2010-12-30 wenzelm 2010-12-30 tuned isatest settings;
2010-12-29 wenzelm 2010-12-29 merged
2010-12-29 krauss 2010-12-29 more robust decomposition of simultaneous goals
2010-12-29 krauss 2010-12-29 function (default) is legacy feature
2010-12-29 wenzelm 2010-12-29 more scalable Symbol_Pos.explode;
2010-12-29 wenzelm 2010-12-29 tuned ML toplevel pp for type string: observe depth limit;
2010-12-29 wenzelm 2010-12-29 theory loader: implicit load path is considered legacy;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-29 wenzelm 2010-12-29 check_file: secondary load path is legacy feature;
2010-12-29 wenzelm 2010-12-29 share_common_data dummy;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy;
2010-12-29 wenzelm 2010-12-29 tuned comments;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy; more accurate dependencies;
2010-12-28 wenzelm 2010-12-28 made SML/NJ happy;
2010-12-27 krauss 2010-12-27 function (tailrec) is a legacy feature
2010-12-25 krauss 2010-12-25 dropped duplicate unused lemmas; spelling
2010-12-25 krauss 2010-12-25 partial_function (tailrec) replaces function (tailrec); dropped unnecessary domain reasoning; curried polydivide_aux
2010-12-24 huffman 2010-12-24 remove lemma ideal_completion.principal_induct2, use principal_induct twice instead