src/HOL/IsaMakefile
2007-06-06 chaieb New Reflected Presburger added to HOL/ex
2007-06-05 wenzelm added ex/Groebner_Examples.thy;
2007-06-05 chaieb Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
2007-06-05 wenzelm Semiring normalization and Groebner Bases.
2007-06-05 haftmann merged Code_Generator.thy into HOL.thy
2007-06-05 urbanc included Class.thy in the compiling process for Nominal/Examples
2007-06-03 wenzelm HOL-ex: tuned deps;
2007-06-01 webertj tuned
2007-06-01 webertj some tests for arith added
2007-06-01 nipkow Moved list comprehension into List
2007-05-31 wenzelm moved IsaPlanner from Provers to Tools;
2007-05-31 wenzelm moved Integ files to canonical place;
2007-05-31 wenzelm moved TFL files to canonical place;
2007-05-31 wenzelm moved Integ files to canonical place;
2007-05-31 urbanc included new example in the compiling process
2007-05-25 nipkow Added List_Comprehension
2007-05-25 urbanc took out Class.thy from the compiling process until memory problems are solved
2007-05-22 huffman remove obsolete CSeries.thy
2007-05-18 haftmann dropped word_setup.ML
2007-05-17 krauss updated
2007-05-15 chaieb A verified theory for rational numbers representation and simple calculations;
2007-05-14 haftmann reorganized float arithmetic
2007-05-13 haftmann added modules rat.ML and int.ML
2007-05-09 wenzelm removed Complex/ComplexBin.thy;
2007-05-06 haftmann dropped HOL.ML
2007-04-27 urbanc alternative and much simpler proof for Church-Rosser of Beta-Reduction
2007-04-26 wenzelm removed legacy ML files;
2007-04-26 haftmann moved code generation pretty integers and characters to separate theories
2007-04-24 berghofe Added datatype_case.ML and nominal_fresh_fun.ML.
2007-04-13 ballarin New file for locale regression tests.
less more (0) -300 -100 -50 -30 tip