src/HOL/IsaMakefile
2007-06-05 urbanc 2007-06-05 included Class.thy in the compiling process for Nominal/Examples
2007-06-03 wenzelm 2007-06-03 HOL-ex: tuned deps;
2007-06-01 webertj 2007-06-01 tuned
2007-06-01 webertj 2007-06-01 some tests for arith added
2007-06-01 nipkow 2007-06-01 Moved list comprehension into List
2007-05-31 wenzelm 2007-05-31 moved IsaPlanner from Provers to Tools; moved Compute_Oracle from Pure/Tools to Tools;
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;
2007-05-31 wenzelm 2007-05-31 moved TFL files to canonical place;
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;
2007-05-31 urbanc 2007-05-31 included new example in the compiling process
2007-05-25 nipkow 2007-05-25 Added List_Comprehension
2007-05-25 urbanc 2007-05-25 took out Class.thy from the compiling process until memory problems are solved
2007-05-22 huffman 2007-05-22 remove obsolete CSeries.thy
2007-05-18 haftmann 2007-05-18 dropped word_setup.ML
2007-05-17 krauss 2007-05-17 updated
2007-05-15 chaieb 2007-05-15 A verified theory for rational numbers representation and simple calculations; verified with respect to the real numbers;
2007-05-14 haftmann 2007-05-14 reorganized float arithmetic
2007-05-13 haftmann 2007-05-13 added modules rat.ML and int.ML
2007-05-09 wenzelm 2007-05-09 removed Complex/ComplexBin.thy;
2007-05-06 haftmann 2007-05-06 dropped HOL.ML
2007-04-27 urbanc 2007-04-27 alternative and much simpler proof for Church-Rosser of Beta-Reduction
2007-04-26 wenzelm 2007-04-26 removed legacy ML files;
2007-04-26 haftmann 2007-04-26 moved code generation pretty integers and characters to separate theories
2007-04-24 berghofe 2007-04-24 Added datatype_case.ML and nominal_fresh_fun.ML.
2007-04-13 ballarin 2007-04-13 New file for locale regression tests.
2007-04-13 huffman 2007-04-13 moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
2007-04-12 huffman 2007-04-12 moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
2007-04-11 huffman 2007-04-11 moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
2007-03-27 haftmann 2007-03-27 cleaned up HOL/ex/Code*.thy
2007-03-26 haftmann 2007-03-26 cleaned up Library( and ex/
2007-03-23 haftmann 2007-03-23 removed outdated example
2007-03-20 haftmann 2007-03-20 dropped OrderedGroup.ML
2007-03-16 haftmann 2007-03-16 dropped LOrder.thy
2007-03-16 urbanc 2007-03-16 adjusted for the example file SOS.thy
2007-02-28 krauss 2007-02-28 more cleanup
2007-02-26 krauss 2007-02-26 Added formalization of size-change principle (experimental).
2007-02-16 krauss 2007-02-16 updated Makefile
2007-02-13 berghofe 2007-02-13 Added new file Nominal/nominal_inductive.ML
2007-02-07 berghofe 2007-02-07 Added Predicate theory.
2007-02-06 urbanc 2007-02-06 corrected typo introduced by me
2007-02-06 urbanc 2007-02-06 moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions
2007-01-22 krauss 2007-01-22 Included ex/Fundefs.thy in HOL-ex session
2007-01-22 krauss 2007-01-22 * Preliminary implementation of tail recursion * Clarified internal interfaces
2007-01-20 wenzelm 2007-01-20 added HOL/ex/Binary.thy;
2007-01-19 wenzelm 2007-01-19 HOL-Lambda: usedir -m no_brackets;
2007-01-16 urbanc 2007-01-16 fixed typo introduced by me
2007-01-16 urbanc 2007-01-16 formalisation of Crary's chapter on logical relations (in the book on Advanced Topics in Type Systems) done by Narboux and Urban
2007-01-16 haftmann 2007-01-16 refined and added example for ExecutableRat
2007-01-03 paulson 2007-01-03 first version of structured proof reconstruction
2006-12-27 haftmann 2006-12-27 added code generator test theory
2006-12-16 huffman 2006-12-16 removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy
2006-12-14 huffman 2006-12-14 remove Hyperreal/fuf.ML
2006-12-12 huffman 2006-12-12 Hyperreal/FrechetDeriv.thy
2006-12-10 wenzelm 2006-12-10 added Tools/string_syntax.ML; tuned;
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-12-04 wenzelm 2006-12-04 converted legacy ML script;
2006-12-02 wenzelm 2006-12-02 TLA: converted legacy ML scripts;
2006-11-27 berghofe 2006-11-27 Added nominal_primrec.ML
2006-11-20 wenzelm 2006-11-20 HOL-Prolog: converted legacy ML scripts;
2006-11-19 wenzelm 2006-11-19 HOL-Algebra: converted legacy ML scripts;