src/HOL/IsaMakefile
2006-09-19 wenzelm 2006-09-19 moved Import/susp.ML to Pure/General;
2006-09-19 haftmann 2006-09-19 added OperationalEquality.thy
2006-09-19 huffman 2006-09-19 add Real/RealVector.thy
2006-09-14 krauss 2006-09-14 updated makefile
2006-08-30 haftmann 2006-08-30 added yet another code generator example
2006-08-29 haftmann 2006-08-29 added typecopy_package and some examples
2006-08-21 haftmann 2006-08-21 added some codegen examples/applications
2006-08-14 haftmann 2006-08-14 added new files
2006-08-08 haftmann 2006-08-08 added Tools/typedef_codegen.ML
2006-08-03 wenzelm 2006-08-03 added HOL/ex/Reflection;
2006-08-03 ballarin 2006-08-03 Restructured algebra library, added ideals and quotient rings.
2006-07-04 wenzelm 2006-07-04 added ex/Guess.thy;
2006-06-23 paulson 2006-06-23 Introduction of Ramsey's theorem
2006-06-11 dixon 2006-06-11 updated IsaMakefiles for new location of IsaPlanner.
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2006-06-04 mengj 2006-06-04 Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
2006-05-16 wenzelm 2006-05-16 added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
2006-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
2006-04-28 berghofe 2006-04-28 Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
2006-04-28 berghofe 2006-04-28 Added new targets for nominal datatype package.
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2006-04-10 nipkow 2006-04-10 Hoare(Parallel) dependencies on document/*
2006-03-10 schirmer 2006-03-10 Added Library/AssocList.thy
2006-03-07 obua 2006-03-07 Added HOL-ZF to Isabelle.
2006-03-07 mengj 2006-03-07 Merged res_atp_setup.ML into res_atp.ML.
2006-03-01 mengj 2006-03-01 Added file Tools/res_atpset.ML.
2006-02-17 wenzelm 2006-02-17 removed Import/lazy_scan.ML;
2006-02-16 wenzelm 2006-02-16 added ex/Abstract_NAT.thy;
2006-02-14 haftmann 2006-02-14 added theory of executable rational numbers
2006-02-01 paulson 2006-02-01 new and updated protocol proofs by Giamp Bella
2006-01-27 mengj 2006-01-27 Added in new file Tools/ATP/reduce_axiomsN.ML
2006-01-06 wenzelm 2006-01-06 removed obsolete eqrule_HOL_data.ML;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-22 wenzelm 2005-12-22 added Provers/project_rule.ML
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-16 paulson 2005-12-16 hashing to eliminate the output of duplicate clauses
2005-12-14 webertj 2005-12-14 ex/Sudoku.thy
2005-12-13 wenzelm 2005-12-13 added HOL/Library/Coinductive_List.thy;
2005-10-28 mengj 2005-10-28 Added Tools/res_hol_clause.ML
2005-10-21 mengj 2005-10-21 Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-19 wenzelm 2005-10-19 removed obsolete HOL/thy_syntax.ML;
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-14 paulson 2005-10-14 deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-10-08 wenzelm 2005-10-08 added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
2005-10-07 wenzelm 2005-10-07 removed obsolete ex/Tuple.thy;
2005-09-29 wenzelm 2005-09-29 HOL4 image is back;
2005-09-26 obua 2005-09-26 added entry for running HOLLight
2005-09-25 berghofe 2005-09-25 Added ExecutableSet and Taylor.
2005-09-23 webertj 2005-09-23 new sat tactic imports resolution proofs from zChaff
2005-09-23 wenzelm 2005-09-23 tuned order of targets;
2005-09-21 wenzelm 2005-09-21 HOL-Complex-Matrix: fixed deps;
2005-09-20 wenzelm 2005-09-20 HOL-ex: Library/Commutative_Ring.thy;
2005-09-20 wenzelm 2005-09-20 moved Tools/comm_ring.ML to Library;
2005-09-20 wenzelm 2005-09-20 removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
2005-09-19 obua 2005-09-19 Removed superfluous HOL/Matrix/cplex/ROOT.ML.
2005-09-19 paulson 2005-09-19 further simplification of the Isabelle-ATP linkup
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems