src/HOL/IsaMakefile
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
2004-12-09 paulson 2004-12-09 converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
2004-12-09 paulson 2004-12-09 converted Datatype_Universe to new-style theory
2004-12-08 paulson 2004-12-08 converted Lfp to new-style theory
2004-12-07 paulson 2004-12-07 converted Gfp to new-style theory
2004-12-02 paulson 2004-12-02 new CLAUSIFY attribute for proof reconstruction with lemmas
2004-11-30 paulson 2004-11-30 resolution package tools by Jia Meng
2004-11-30 paulson 2004-11-30 converted Wellfounded_Relations to Isar script
2004-11-29 paulson 2004-11-29 converted to Isar script, simplifying some results
2004-11-24 berghofe 2004-11-24 Added Library/EfficientNat
2004-11-19 paulson 2004-11-19 moved and renamed Integ/Equiv.thy
2004-11-19 chaieb 2004-11-19 Barith removed VS: ----------------------------------------------------------------------
2004-10-06 chaieb 2004-10-06 changed in order to insert Barith.thy
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-09-03 obua 2004-09-03 Matrix theory, linear programming
2004-09-02 paulson 2004-09-02 new example of a quotiented nested data type
2004-08-20 paulson 2004-08-20 fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
2004-08-03 ballarin 2004-08-03 New transitivity reasoners for transitivity only and quasi orders.
2004-07-31 paulson 2004-07-31 conversion of Hyperreal/{Fact,Filter} to Isar scripts
2004-07-30 paulson 2004-07-30 conversion of Integration and NSPrimes to Isar scripts
2004-07-28 paulson 2004-07-28 conversion of SEQ.ML to Isar script
2004-07-28 paulson 2004-07-28 conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2004-07-16 nipkow 2004-07-16 added Complex/root
2004-07-12 nipkow 2004-07-12 *** empty log message ***
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-29 obua 2004-06-29 support for sparse matrices
2004-05-29 wenzelm 2004-05-29 target 'generate';
2004-05-19 paulson 2004-05-19 conversion of Hilbert_Choice to Isar script
2004-05-18 obua 2004-05-18 Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-07 bauerg 2004-05-07 *** empty log message ***
2004-04-23 wenzelm 2004-04-23 HOL-Matrix: document setup;