src/HOL/IsaMakefile
2006-11-20 wenzelm 2006-11-20 HOL-Prolog: converted legacy ML scripts;
2006-11-19 wenzelm 2006-11-19 HOL-Algebra: converted legacy ML scripts;
2006-11-13 krauss 2006-11-13 added lexicographic_order.ML to makefile
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-11-08 haftmann 2006-11-08 renamed Lattice_Locales to Lattices
2006-11-08 wenzelm 2006-11-08 removed NatArith.thy, Main.ML;
2006-11-06 haftmann 2006-11-06 added state monad to HOL library
2006-11-04 huffman 2006-11-04 new Deriv.thy contains stuff from Lim.thy
2006-11-03 haftmann 2006-11-03 simplified reasoning tools setup
2006-11-01 urbanc 2006-11-01 changed to not compile Iteration and Recursion, but Lam_Funs instead
2006-10-26 paulson 2006-10-26 Conversion to clause form now tolerates Boolean variables without looping. Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted
2006-10-23 berghofe 2006-10-23 Added Compile and Height examples to Nominal directory.
2006-10-20 haftmann 2006-10-20 removed antisym_setup.ML
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-13 berghofe 2006-10-13 Added new package for inductive definitions, moved old package to old_inductive_package.ML
2006-10-06 kleing 2006-10-06 examples for hex and bin numerals
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-10-01 wenzelm 2006-10-01 moved Infinite_Set.thy to Library; removed obsolete ex/StringEx.thy; renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
2006-09-29 wenzelm 2006-09-29 moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
2006-09-28 wenzelm 2006-09-28 removed obsolete Real/document/root.tex; removed obsolete Isar_examples/Cantor.ML; renamed Real/Float.ML to Real/float.ML;
2006-09-28 paulson 2006-09-28 clearout of obsolete code
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