src/HOL/IsaMakefile
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.
2005-04-19 paulson 2005-04-19 more tidying of libraries in Reconstruction
2005-04-19 paulson 2005-04-19 restored the target HOL-Complex-Import
2005-04-14 nipkow 2005-04-14 Removed dir Orderings in Library
2005-04-11 paulson 2005-04-11 removal of Main and other tidying up
2005-04-08 paulson 2005-04-08 Reconstruction code, now packaged to avoid name clashes
2005-04-07 quigley 2005-04-07 Reconstruction.thy and IsaMakefile updated
2005-04-04 quigley 2005-04-04 Updated to add watcher code.
2005-04-01 skalberg 2005-04-01 Updated import configuration.
2005-03-29 paulson 2005-03-29 converted HOL-Subst to tactic scripts
2005-03-24 ballarin 2005-03-24 Transitivity reasoner ignores types amenable to linear arithmetic. These are currently nat, int, real. Fixed IsaMakefile.
2005-03-24 paulson 2005-03-24 COMMENT IN WRONG PLACE
2005-03-23 paulson 2005-03-23 temporary removal of Import
2005-03-07 obua 2005-03-07 Cleaning up HOL/Matrix
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-09 nipkow 2005-02-09 added lattice_locales
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-17 paulson 2004-12-17 removed two looping simplifications in SetInterval.thy; deleted the .ML file
2004-12-15 paulson 2004-12-15 removal of HOL_Lemmas
2004-12-14 paulson 2004-12-14 converted Relation_Power to new-style theory
2004-12-13 paulson 2004-12-13 removal of NatArith.ML and Product_Type.ML