2010-09-02 blanchet 2010-09-02 merged
2010-08-31 blanchet 2010-08-31 move file
2010-08-31 blanchet 2010-08-31 shorten a few file names
2010-09-01 haftmann 2010-09-01 factored out generic part of Scala serializer into code_namespace.ML
2010-09-01 bulwahn 2010-09-01 merged
2010-08-31 bulwahn 2010-08-31 adding Lambda example theory; tuned
2010-08-31 blanchet 2010-08-31 "try" -- a new diagnosis tool that tries to apply several methods in parallel
2010-08-25 bulwahn 2010-08-25 adding hotel keycard example for prolog generation
2010-08-23 hoelzl 2010-08-23 Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions
2010-08-18 haftmann 2010-08-18 removed separate quickcheck_record module
2010-08-17 haftmann 2010-08-17 dropped SML typedef_codegen: does not fit to code equations for record operations any longer
2010-08-17 haftmann 2010-08-17 deleted typecopy package
2010-08-12 haftmann 2010-08-12 moved Record.thy from session Plain to Main; avoid variable name acc
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-03 wenzelm 2010-08-03 renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
2010-08-01 bulwahn 2010-08-01 adding Code_Prolog theory to IsaMakefile and HOL-Library root file
2010-07-29 bulwahn 2010-07-29 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
2010-07-28 blanchet 2010-07-28 consequence of directory renaming
2010-07-27 blanchet 2010-07-27 rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come
2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-07-26 haftmann 2010-07-26 added Code_Natural.thy
2010-07-21 bulwahn 2010-07-21 merged
2010-07-21 bulwahn 2010-07-21 added new theories to IsaMakefile and ROOT.ML
2010-07-21 wenzelm 2010-07-21 merged
2010-07-19 haftmann 2010-07-19 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
2010-07-21 wenzelm 2010-07-21 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
2010-07-14 haftmann 2010-07-14 load cache_io before code generator; moved adhoc-overloading to generic tools
2010-07-13 krauss 2010-07-13 uniform do notation for monads
2010-07-13 krauss 2010-07-13 generic ad-hoc overloading via check/uncheck
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-07-12 wenzelm 2010-07-12 removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years;
2010-07-12 haftmann 2010-07-12 dropped empty theory
2010-07-12 haftmann 2010-07-12 split off mrec into separate theory
2010-07-12 haftmann 2010-07-12 merged
2010-07-12 haftmann 2010-07-12 more regular session structure
2010-07-10 wenzelm 2010-07-10 regular image setup for HOL-Library (cf. 4915de09b4d3 and ccae4ecd67f4) -- note that document preparation requires a separate session directory, and library.ML is a bit too generic as a file in the default load path;
2010-07-09 krauss 2010-07-09 moved example to its own file in HOL/ex
2010-07-08 haftmann 2010-07-08 more accurate dependencies
2010-07-08 haftmann 2010-07-08 tuned tabs
2010-07-02 haftmann 2010-07-02 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
2010-07-01 wenzelm 2010-07-01 avoid Old_Number_Theory; more precise dependencies;
2010-07-01 hoelzl 2010-07-01 Add theory for indicator function.
2010-07-01 haftmann 2010-07-01 repaired line ending
2010-06-30 haftmann 2010-06-30 one unified Word theory
2010-06-30 haftmann 2010-06-30 more speaking names
2010-06-30 haftmann 2010-06-30 more speaking theory names
2010-06-25 blanchet 2010-06-25 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 blanchet 2010-06-25 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-24 wenzelm 2010-06-24 more accurate dependencies;
2010-06-22 blanchet 2010-06-22 factor out TPTP format output into file of its own, to facilitate further changes
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-06-02 wenzelm 2010-06-02 replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;
2010-06-02 haftmann 2010-06-02 HOL-Proofs is based in Main.thy
2010-05-25 wenzelm 2010-05-25 moved ML files where they are actually used; more precise dependencies;
2010-05-25 wenzelm 2010-05-25 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
2010-05-20 haftmann 2010-05-20 renamed List_Set to the now more appropriate More_Set