src/HOL/IsaMakefile
2009-09-10 haftmann 2009-09-10 obey underscore naming convention
2009-09-10 haftmann 2009-09-10 generic transfer procedure
2009-09-04 boehmes 2009-09-04 tuned
2009-09-02 boehmes 2009-09-02 merged
2009-09-02 boehmes 2009-09-02 moved Mirabelle from HOL/Tools to HOL, added session HOL-Mirabelle
2009-09-02 wenzelm 2009-09-02 reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-08-26 boehmes 2009-08-26 added further conversions and conversionals
2009-08-21 krauss 2009-08-21 fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)
2009-08-06 wenzelm 2009-08-06 misc changes to SOS by Philipp Meyer: CSDP_EXE as central setting; separate component src/HOL/Library/Sum_Of_Squares; misc tuning and rearrangement of neos_csdp_client; more robust treatment of shell paths; debugging depends on local flag; removed unused parts;
2009-08-04 wenzelm 2009-08-04 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
2009-07-31 boehmes 2009-07-31 added Mirabelle
2009-07-23 chaieb 2009-07-23 merged
2009-07-15 chaieb 2009-07-15 Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed.
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-07-10 krauss 2009-07-10 move Kleene_Algebra to Library
2009-07-03 haftmann 2009-07-03 nominal.ML is nominal_datatype.ML
2009-06-29 haftmann 2009-06-29 renamed theory Code_Set to Fset
2009-06-25 haftmann 2009-06-25 added List_Set and Code_Set theories
2009-06-24 wenzelm 2009-06-24 standard naming conventions for session and theories;
2009-06-23 haftmann 2009-06-23 NewNumberTheory depends on Algebra
2009-06-23 chaieb 2009-06-23 Added Library/Fraction_Field.thy: The fraction field of any integral domain
2009-06-22 wenzelm 2009-06-22 observe standard theory naming conventions; modernized headers;
2009-06-21 nipkow 2009-06-21 fixed NewNumberTheory deps
2009-06-19 haftmann 2009-06-19 merged
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-19 nipkow 2009-06-19 Added NewNumberTheory by Jeremy Avigad
2009-06-17 huffman 2009-06-17 new GCD library, courtesy of Jeremy Avigad
2009-06-10 haftmann 2009-06-10 separate directory for datatype package
2009-06-09 haftmann 2009-06-09 first running version of qc generators for datatypes
2009-06-04 haftmann 2009-06-04 added trees implementing mappings
2009-06-02 haftmann 2009-06-02 tuned code generator test theories
2009-06-02 berghofe 2009-06-02 merged
2009-06-02 berghofe 2009-06-02 Added Convex_Euclidean_Space.thy again.
2009-06-01 huffman 2009-06-01 add dependency on Limits.thy
2009-05-28 himmelma 2009-05-28 Removed Convex_Euclidean_Space.thy from Library.
2009-05-28 himmelma 2009-05-28 Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
2009-05-26 haftmann 2009-05-26 separate module for quickcheck generators
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-16 haftmann 2009-05-16 experimental move of Quickcheck and related theories to HOL image
2009-05-15 haftmann 2009-05-15 experimental addition of quickcheck
2009-05-15 haftmann 2009-05-15 dropped theory Term_Of_Syntax
2009-05-12 haftmann 2009-05-12 split Predicate_Compile examples into separate theory
2009-05-12 haftmann 2009-05-12 merged
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-05-12 chaieb 2009-05-12 Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-07 haftmann 2009-05-07 added theory for explicit equivalence relation in preorders
2009-05-06 haftmann 2009-05-06 proper structures for list and string code generation stuff
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2009-05-04 haftmann 2009-05-04 removed code_name module
2009-04-25 wenzelm 2009-04-25 misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;
2009-04-24 haftmann 2009-04-24 observe distinction between Pure/Tools and Tools more closely
2009-04-20 haftmann 2009-04-20 power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
2009-04-15 haftmann 2009-04-15 code generator bootstrap theory src/Tools/Code_Generator.thy
2009-04-15 haftmann 2009-04-15 wrecked old code_funcgr module
2009-04-15 haftmann 2009-04-15 theory NatBin now named Nat_Numeral
2009-03-23 haftmann 2009-03-23 moved Imperative_HOL examples to Imperative_HOL/ex