src/HOL/IsaMakefile
2009-06-04 haftmann 2009-06-04 added trees implementing mappings
2009-06-02 haftmann 2009-06-02 tuned code generator test theories
2009-06-02 berghofe 2009-06-02 merged
2009-06-02 berghofe 2009-06-02 Added Convex_Euclidean_Space.thy again.
2009-06-01 huffman 2009-06-01 add dependency on Limits.thy
2009-05-28 himmelma 2009-05-28 Removed Convex_Euclidean_Space.thy from Library.
2009-05-28 himmelma 2009-05-28 Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
2009-05-26 haftmann 2009-05-26 separate module for quickcheck generators
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-16 haftmann 2009-05-16 experimental move of Quickcheck and related theories to HOL image
2009-05-15 haftmann 2009-05-15 experimental addition of quickcheck
2009-05-15 haftmann 2009-05-15 dropped theory Term_Of_Syntax
2009-05-12 haftmann 2009-05-12 split Predicate_Compile examples into separate theory
2009-05-12 haftmann 2009-05-12 merged
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-05-12 chaieb 2009-05-12 Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-05-08 haftmann 2009-05-08 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-07 haftmann 2009-05-07 added theory for explicit equivalence relation in preorders
2009-05-06 haftmann 2009-05-06 proper structures for list and string code generation stuff
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2009-05-04 haftmann 2009-05-04 removed code_name module
2009-04-25 wenzelm 2009-04-25 misc cleanup of auto_solve and quickcheck: tools are in src/Tools and loaded uniformly in HOL; preferences are configured in their proper place -- despite old misleading comments in the source; use predefined preferences categories; setmp preferences in-place;
2009-04-24 haftmann 2009-04-24 observe distinction between Pure/Tools and Tools more closely
2009-04-20 haftmann 2009-04-20 power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
2009-04-15 haftmann 2009-04-15 code generator bootstrap theory src/Tools/Code_Generator.thy
2009-04-15 haftmann 2009-04-15 wrecked old code_funcgr module
2009-04-15 haftmann 2009-04-15 theory NatBin now named Nat_Numeral
2009-03-23 haftmann 2009-03-23 moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-22 haftmann 2009-03-22 dropped theory Arith_Tools
2009-03-12 haftmann 2009-03-12 merged
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-12 nipkow 2009-03-12 optional latex sugar
2009-03-11 wenzelm 2009-03-11 basic setup for "main" as generated Isabelle manual;
2009-03-11 nipkow 2009-03-11 merged
2009-03-11 nipkow 2009-03-11 Docs
2009-03-11 haftmann 2009-03-11 moved Decision_Procs examples to Decision_Procs/ex
2009-03-09 wenzelm 2009-03-09 added session HOL-Docs;
2009-03-08 haftmann 2009-03-08 added predicate compiler, as formally checked prototype, not as user package
2009-03-06 haftmann 2009-03-06 constructive version of Cantor's first diagonalization argument
2009-03-04 chaieb 2009-03-04 Added Libray dependency on Topology_Euclidean_Space
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2009-02-28 wenzelm 2009-02-28 A Serbian theory, by Filip Maric.
2009-02-28 wenzelm 2009-02-28 moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28 wenzelm 2009-02-28 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-26 wenzelm 2009-02-26 merged
2009-02-25 huffman 2009-02-25 new theory of Archimedean fields
2009-02-22 haftmann 2009-02-22 formal dependency on newly emerging algorithm
2009-02-20 huffman 2009-02-20 add theory of products as real vector spaces to Library
2009-02-20 huffman 2009-02-20 add new theory Product_plus.thy to Library
2009-02-19 huffman 2009-02-19 add formalization of a type of integers mod 2 to Library
2009-02-19 huffman 2009-02-19 new theory of real inner product spaces
2009-02-18 huffman 2009-02-18 move Polynomial.thy to Library
2009-02-18 huffman 2009-02-18 move FrechetDeriv.thy to Library
2009-02-18 huffman 2009-02-18 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-13 nipkow 2009-02-13 Moved Nat_Int_Bij into Library
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.