src/HOL/IsaMakefile
2009-10-26 wenzelm 2009-10-26 recovered sort indentation for "sort position", as documented in the file; more precise dependencies -- HOL-Multivariate_Analysis produces an image; tuned;
2009-10-26 blanchet 2009-10-26 merged
2009-10-26 blanchet 2009-10-26 merged
2009-10-26 blanchet 2009-10-26 merged
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.
2009-10-26 berghofe 2009-10-26 merged
2009-10-26 berghofe 2009-10-26 Added Pattern.thy to Nominal/Examples.
2009-10-26 wenzelm 2009-10-26 more precise dependencies, notably for HOL-Multivariate_Analysis;
2009-10-26 haftmann 2009-10-26 merged
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis
2009-10-23 krauss 2009-10-23 renamed auto_term.ML -> relation.ML
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-10-23 krauss 2009-10-23 renamed FundefDatatype -> Function_Fun
2009-10-23 haftmann 2009-10-23 merged
2009-10-23 haftmann 2009-10-23 turned off old quickcheck
2009-10-23 krauss 2009-10-23 pat_completeness gets its own file
2009-10-20 wenzelm 2009-10-20 modernized session SET_Protocol;
2009-10-20 wenzelm 2009-10-20 modernized session Metis_Examples;
2009-10-20 wenzelm 2009-10-20 modernized session Isar_Examples;
2009-10-20 wenzelm 2009-10-20 more accurate dependencies for HOL-SMT, which is a session with image; misc cleanup;
2009-10-20 boehmes 2009-10-20 added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)
2009-10-01 wenzelm 2009-10-01 more precise dependencies;
2009-09-28 wenzelm 2009-09-28 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-24 bulwahn 2009-09-24 merged; adopted to changes from Code_Evaluation in the predicate compiler
2009-09-23 bulwahn 2009-09-23 moved predicate compiler to Tools
2009-09-23 bulwahn 2009-09-23 handling of definitions
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-09-21 haftmann 2009-09-21 added session theory for Bali and Nominal_Examples
2009-09-21 haftmann 2009-09-21 added session entry point theories
2009-09-21 haftmann 2009-09-21 entry point theory for examples; reactivated half-dead example
2009-09-21 haftmann 2009-09-21 theory entry point for session Hoare_Parallel (now also with proper underscore)
2009-09-18 boehmes 2009-09-18 added new method "smt": an oracle-based connection to external SMT solvers
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