2008-03-02 nipkow 2008-03-02 Generalized Zorn and added well-ordering theorem
2008-03-01 wenzelm 2008-03-01 tuned ML code, more antiquotations;
2008-03-01 wenzelm 2008-03-01 misc cleanup of embedded ML code; use more antiquotations; tuned;
2008-03-01 wenzelm 2008-03-01 added @{const} antiquotation;
2008-03-01 wenzelm 2008-03-01 use more antiquotations;
2008-02-28 wenzelm 2008-02-28 unused_thms: print via official context (ProofContext.pretty_fact), not just the theory certificate (Display.pretty_thm); tuned;
2008-02-28 berghofe 2008-02-28 Added function for finding unused theorems.
2008-02-28 berghofe 2008-02-28 Added unused_thms command.
2008-02-28 haftmann 2008-02-28 import all 'special code' types
2008-02-28 haftmann 2008-02-28 added code generator setup
2008-02-28 wenzelm 2008-02-28 Transitive_Closure: induct and cases rules now declare proper case_names;
2008-02-28 wenzelm 2008-02-28 Transitive_Closure: induct and cases rules now declare proper case_names; tuned;
2008-02-28 wenzelm 2008-02-28 rtranclp_induct, tranclp_induct: added case_names; tuned proofs;
2008-02-28 nipkow 2008-02-28 tuned
2008-02-28 wenzelm 2008-02-28 removed legacy ML bindings;
2008-02-28 wenzelm 2008-02-28 tuned syntax declaration;
2008-02-28 wenzelm 2008-02-28 wf_trancl: structured proof; tuned proofs; removed legacy ML bindings;
2008-02-28 wenzelm 2008-02-28 rtranclE, tranclE: tuned statement, added case_names;
2008-02-28 wenzelm 2008-02-28 renamed ListSpace to ListVector;
2008-02-28 wenzelm 2008-02-28 added HOL-Library;
2008-02-27 wenzelm 2008-02-27 more precise handling of "group" for termination;
2008-02-27 haftmann 2008-02-27 added theories for imperative HOL
2008-02-27 haftmann 2008-02-27 added theory for countable types
2008-02-27 haftmann 2008-02-27 added theory for reflected types
2008-02-27 haftmann 2008-02-27 proper merge of base sorts
2008-02-27 nipkow 2008-02-27 Renamed ListSpace to ListVector
2008-02-27 chaieb 2008-02-27 Fixed dependency on Dense_Linear_Order
2008-02-27 schirmer 2008-02-27 removed some debugging output from trace
2008-02-27 chaieb 2008-02-27 Loads Dense_Linear_Order (needed dlo_simps)
2008-02-27 chaieb 2008-02-27 Fixed dependencies for proofs -- ferrack needed
2008-02-27 chaieb 2008-02-27 Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
2008-02-27 chaieb 2008-02-27 fixed dependencies
2008-02-27 chaieb 2008-02-27 Removed theorems from default simpset
2008-02-27 chaieb 2008-02-27 Fixed proofs
2008-02-27 chaieb 2008-02-27 Loads Dense_Linear_Order.thy
2008-02-27 chaieb 2008-02-27 loads Tools/Qelim/qelim.ML
2008-02-27 chaieb 2008-02-27 HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
2008-02-27 chaieb 2008-02-27 Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy
2008-02-26 haftmann 2008-02-26 other UNIV lemmas
2008-02-26 haftmann 2008-02-26 some more primrec
2008-02-26 haftmann 2008-02-26 class itself works around a problem with class interpretation in class finite
2008-02-26 haftmann 2008-02-26 moved some set lemmas from Set.thy here
2008-02-26 haftmann 2008-02-26 tuned heading
2008-02-26 haftmann 2008-02-26 char and nibble are finite
2008-02-26 haftmann 2008-02-26 moved some set lemmas to Set.thy
2008-02-26 haftmann 2008-02-26 tuned proofs
2008-02-26 wenzelm 2008-02-26 tuned document; tuned proofs;
2008-02-26 wenzelm 2008-02-26 tuned document;
2008-02-26 bulwahn 2008-02-26 Added useful general lemmas from the work with the HeapMonad
2008-02-26 haftmann 2008-02-26 some steps towards automated generators
2008-02-26 haftmann 2008-02-26 operation collapse
2008-02-26 haftmann 2008-02-26 Zero/Suc recursion combinator for type index
2008-02-26 haftmann 2008-02-26 added accidental omissions
2008-02-25 wenzelm 2008-02-25 thm_deps: sort result;
2008-02-25 wenzelm 2008-02-25 tuned msg;
2008-02-25 wenzelm 2008-02-25 fixed ChangeLog.gz path;
2008-02-25 wenzelm 2008-02-25 fixed document;
2008-02-25 wenzelm 2008-02-25 welcome: actually check for ChangeLog.gz; tuned structure Distribution;
2008-02-25 wenzelm 2008-02-25 tuned structure Distribution;
2008-02-25 wenzelm 2008-02-25 implicit use of LocalTheory.group etc.;