src/HOL/IsaMakefile
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
2004-01-29 paulson 2004-01-29 simplifications in the hyperreals
2004-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
2004-01-28 paulson 2004-01-28 converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-14 nipkow 2004-01-14 Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-23 paulson 2003-12-23 converting Hyperreal/NthRoot to Isar
2003-12-23 paulson 2003-12-23 converting Complex/Complex.ML to Isar
2003-12-23 paulson 2003-12-23 tidying up hcomplex arithmetic
2003-12-22 paulson 2003-12-22 converted Complex/NSComplex to Isar script
2003-12-22 paulson 2003-12-22 moving HyperArith0.ML to other theories
2003-12-17 paulson 2003-12-17 converted Hyperreal/HyperDef to Isar script
2003-12-16 paulson 2003-12-16 converted Hyperreal/HyperOrd to new-style theory
2003-12-10 paulson 2003-12-10 combining Real/{RealArith0,real_arith}.ML
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc