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
2010-05-20 haftmann 2010-05-20 adjusted
2010-05-17 haftmann 2010-05-17 dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-15 wenzelm 2010-05-15 moved normarith.ML where it is actually used; less inaccurate dependencies;
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
2010-05-15 wenzelm 2010-05-15 more precise dependencies for HOL-Word-SMT_Examples;
2010-05-14 blanchet 2010-05-14 move Refute dependency from Plain to Main
2010-05-14 blanchet 2010-05-14 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
2010-05-13 boehmes 2010-05-13 more precise dependencies
2010-05-12 boehmes 2010-05-12 updated SMT certificates
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12 boehmes 2010-05-12 integrated SMT into the HOL image
2010-05-12 boehmes 2010-05-12 split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
2010-05-12 boehmes 2010-05-12 added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
2010-05-12 boehmes 2010-05-12 deleted SMT translation files (to be replaced by a simplified version)
2010-05-12 boehmes 2010-05-12 move the addition of extra facts into a separate module
2010-05-11 huffman 2010-05-11 no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-11 haftmann 2010-05-11 merged
2010-05-10 haftmann 2010-05-10 updated references to ML files
2010-05-10 haftmann 2010-05-10 less complex organization of cooper source code
2010-05-10 huffman 2010-05-10 new construction of real numbers using Cauchy sequences
2010-05-10 huffman 2010-05-10 put construction of reals using Dedekind cuts in HOL/ex
2010-05-07 haftmann 2010-05-07 renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-06 haftmann 2010-05-06 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-05-04 hoelzl 2010-05-04 Corrected imports; better approximation of dependencies.
2010-05-04 hoelzl 2010-05-04 Add Convex to Library build
2010-04-29 huffman 2010-04-29 merged
2010-04-28 huffman 2010-04-28 move path-related stuff into new theory file
2010-04-28 huffman 2010-04-28 add new Multivariate_Analysis files to IsaMakefile
2010-04-29 Cezary Kaliszyk 2010-04-29 Tuning the quotient examples
2010-04-26 blanchet 2010-04-26 merge
2010-04-23 blanchet 2010-04-23 now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
2010-04-23 blanchet 2010-04-23 move the minimizer to the Sledgehammer directory
2010-04-24 huffman 2010-04-24 document generation for Multivariate_Analysis
2010-04-24 huffman 2010-04-24 move l2-norm stuff into separate theory file
2010-04-23 wenzelm 2010-04-23 removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;
2010-04-23 Cezary Kaliszyk 2010-04-23 Finite set theory
2010-04-22 wenzelm 2010-04-22 split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
2010-04-15 haftmann 2010-04-15 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-04-11 haftmann 2010-04-11 removed rather toyish tree
2010-04-08 bulwahn 2010-04-08 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
2010-04-07 hoelzl 2010-04-07 Added Information theory and Example: dining cryptographers
2010-04-01 wenzelm 2010-04-01 slightly more standard dependencies;
2010-04-01 blanchet 2010-04-01 merged
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used