2009-03-23 ago moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-22 ago dropped theory Arith_Tools
2009-03-12 ago merged
2009-03-12 ago vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-12 ago optional latex sugar
2009-03-11 ago basic setup for "main" as generated Isabelle manual;
2009-03-11 ago merged
2009-03-11 ago Docs
2009-03-11 ago moved Decision_Procs examples to Decision_Procs/ex
2009-03-09 ago added session HOL-Docs;
2009-03-08 ago added predicate compiler, as formally checked prototype, not as user package
2009-03-06 ago constructive version of Cantor's first diagonalization argument
2009-03-04 ago Added Libray dependency on Topology_Euclidean_Space
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-04 ago Made Option a separate theory and renamed option_map to
2009-02-28 ago A Serbian theory, by Filip Maric.
2009-02-28 ago moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28 ago moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-26 ago merged
2009-02-25 ago new theory of Archimedean fields
2009-02-22 ago formal dependency on newly emerging algorithm
2009-02-20 ago add theory of products as real vector spaces to Library
2009-02-20 ago add new theory Product_plus.thy to Library
2009-02-19 ago add formalization of a type of integers mod 2 to Library
2009-02-19 ago new theory of real inner product spaces
2009-02-18 ago move Polynomial.thy to Library
2009-02-18 ago move FrechetDeriv.thy to Library
2009-02-18 ago split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-13 ago Moved Nat_Int_Bij into Library
2009-02-12 ago Moved FTA into Lib and cleaned it up a little.
2009-02-11 ago Moved Order_Relation into Library and moved some of it into Relation.
2009-02-09 ago added Determinants to Library
2009-02-09 ago added Euclidean_Space and Glbs to Library
2009-02-09 ago Added HOL/Library/Finite_Cartesian_Product.thy to Library
2009-02-06 ago session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-06 ago fixed dependencies : Theory Dense_Linear_Order moved to Library
2009-02-05 ago merged
2009-02-05 ago moved Random.thy to Library
2009-02-05 ago Add approximation method
2009-02-05 ago Added new Float theory and moved old Library/Float.thy to ComputeFloat
2009-02-03 ago merged Big0
2009-02-03 ago established session HOL-Reflection
2009-02-16 ago removed obsolete axclass manual and examples;
2009-02-02 ago added Mapping.thy to Library
2009-01-30 ago fixed case
2009-01-30 ago Added Formal_Power_Series_Examples to HOL-ex image
2009-01-29 ago Inserted Formal_Power_Series.thy under Library
2009-01-28 ago Reflection.thy now in HOL/Library
2009-01-26 ago entry point for Word library now named Word
2009-01-17 ago no document for HOL-Base
2009-01-16 ago added HOL-Base image
2009-01-12 ago add Polynomial.thy to makefile
2009-01-08 ago split of Imperative_HOL theories from HOL-Library
2008-12-29 ago adapted HOL source structure to distribution layout
2008-12-27 ago renamed LexOrds.thy to Termination.thy; examples for sizechange method
2008-12-16 ago method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-12-15 ago merged
2008-12-11 ago Testfile for Stefan's code generator
2008-12-15 ago moved value.ML to src/Tools