src/HOL/IsaMakefile
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;
2004-04-22 paulson 2004-04-22 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate places
2004-04-19 kleing 2004-04-19 renamed HOL-Import-HOL to HOL4, added to images target
2004-04-17 kleing 2004-04-17 added HOL-Matrix, added HOL/Matrix/ROOT.ML
2004-04-16 nipkow 2004-04-16 Moved ring stuff from ex into Ring_and_Field.
2004-04-16 berghofe 2004-04-16 Added theory with examples for quickcheck command.
2004-04-16 wenzelm 2004-04-16 session graph;
2004-04-15 nipkow 2004-04-15 Added ex/Exceptions.thy
2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.
2004-04-08 paulson 2004-04-08 new theory
2004-04-02 skalberg 2004-04-02 Added HOL proof importer.
2004-04-02 webertj 2004-04-02 Tools/sat_solver.ML and Tools/prop_logic.ML added
2004-04-01 paulson 2004-04-01 removal of Binary Trees examples prepratory to its going into AFP
2004-03-31 nipkow 2004-03-31 Lex now in AFP
2004-03-29 skalberg 2004-03-29 Added bitvector library (Word) to HOL/Library and a theory using it (Adder) to HOL/ex.
2004-03-25 kleing 2004-03-25 moved MiniML and AVL to archive of formal proofs
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-03-08 paulson 2004-03-08 new theory of infinite sets
2004-03-06 nipkow 2004-03-06 Lex: removed last ML files
2004-03-05 paulson 2004-03-05 Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
2004-03-04 nipkow 2004-03-04 Lex: ML -> thy
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-04 nipkow 2004-03-04 Removed ML files from Lex
2004-03-02 paulson 2004-03-02 converted Hyperreal/IntFloor to Isar script
2004-03-02 kleing 2004-03-02 converted MiniML to Isar
2004-03-01 paulson 2004-03-01 converted Hyperreal/HTranscendental to Isar script
2004-03-01 kleing 2004-03-01 converted to Isar
2004-02-26 paulson 2004-02-26 converted Hyperreal/Series to Isar script
2004-02-26 paulson 2004-02-26 converted Hyperreal/NatStar to Isar script
2004-02-25 paulson 2004-02-25 converted Hyperreal/HSeries to Isar script
2004-02-24 paulson 2004-02-24 converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
2004-02-23 paulson 2004-02-23 converted HOL/Complex/NSInduct to Isar script
2004-02-23 paulson 2004-02-23 converted HOL/Complex/NSCA to Isar script
2004-02-21 paulson 2004-02-21 conversion of Complex/CStar to Isar script
2004-02-21 paulson 2004-02-21 conversion of Complex/CSeries to Isar script
2004-02-21 paulson 2004-02-21 conversion of Complex/CLim to Isar script
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2004-02-03 paulson 2004-02-03 tidying of the complex numbers
2004-02-02 paulson 2004-02-02 Conversion of HyperNat to Isar format and its declaration as a semiring