src/HOL/IsaMakefile
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
2005-09-17 wenzelm 2005-09-17 generate: added HOL-Complex-Generate-HOLLight;
2005-09-15 huffman 2005-09-15 merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
2005-09-15 wenzelm 2005-09-15 added HOL/ex/Hebrew.thy; tuned;
2005-09-14 wenzelm 2005-09-14 renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
2005-09-14 wenzelm 2005-09-14 tuned;
2005-09-14 chaieb 2005-09-14 The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy comm_ring : a reflected Method for proving equalities in a commutative ring
2005-09-12 huffman 2005-09-12 add file Hyperreal/transfer.ML
2005-09-12 obua 2005-09-12 1) Added target HOL-Complex-Generate-HOLLight 2) Make heap image for HOL-Complex-Matrix
2005-09-07 wenzelm 2005-09-07 removed TLA/Inc/Pcount.thy;
2005-09-07 paulson 2005-09-07 consolidation of watcher.ML and watcher.sig
2005-09-06 huffman 2005-09-06 add Hyperreal dependencies
2005-09-06 wenzelm 2005-09-06 removed some ML files in Modelcheck/;
2005-09-02 paulson 2005-09-02 deleted obsolete VampireCommunication.ML
2005-08-31 wenzelm 2005-08-31 added Complex/ex/BigO_Complex.thy;
2005-08-05 berghofe 2005-08-05 Added Extraction/Pigeonhole.
2005-08-03 avigad 2005-08-03 added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
2005-07-25 avigad 2005-07-25 Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
2005-07-19 obua 2005-07-19 proving bounds for real linear programs
2005-07-13 obua 2005-07-13 - added cplex package to HOL/Matrix
2005-07-12 obua 2005-07-12 - use TableFun instead of homebrew binary tree in am_interpreter.ML - add Floats to HOL/Real
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-06-21 wenzelm 2005-06-21 fixed HOL-Complex-Matrix target;
2005-06-20 wenzelm 2005-06-20 HOL-Matrix: plain session;
2005-06-09 wenzelm 2005-06-09 added Isar_examples/Drinker.thy;
2005-06-02 wenzelm 2005-06-02 renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
2005-05-26 paulson 2005-05-26 goodby to modUnix
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2005-04-28 bauerg 2005-04-28 *** empty log message ***
2005-04-27 kleing 2005-04-27 reverted last change (dependencies in HOL)
2005-04-20 quigley 2005-04-20 Removed remaining references to Main.thy in reconstruction code.