src/HOL/IsaMakefile
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;
2006-11-13 krauss 2006-11-13 added lexicographic_order.ML to makefile
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
2006-11-08 haftmann 2006-11-08 renamed Lattice_Locales to Lattices
2006-11-08 wenzelm 2006-11-08 removed NatArith.thy, Main.ML;
2006-11-06 haftmann 2006-11-06 added state monad to HOL library
2006-11-04 huffman 2006-11-04 new Deriv.thy contains stuff from Lim.thy
2006-11-03 haftmann 2006-11-03 simplified reasoning tools setup
2006-11-01 urbanc 2006-11-01 changed to not compile Iteration and Recursion, but Lam_Funs instead
2006-10-26 paulson 2006-10-26 Conversion to clause form now tolerates Boolean variables without looping. Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted
2006-10-23 berghofe 2006-10-23 Added Compile and Height examples to Nominal directory.
2006-10-20 haftmann 2006-10-20 removed antisym_setup.ML
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-13 berghofe 2006-10-13 Added new package for inductive definitions, moved old package to old_inductive_package.ML
2006-10-06 kleing 2006-10-06 examples for hex and bin numerals
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-10-01 wenzelm 2006-10-01 moved Infinite_Set.thy to Library; removed obsolete ex/StringEx.thy; renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
2006-09-29 wenzelm 2006-09-29 moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
2006-09-28 wenzelm 2006-09-28 removed obsolete Real/document/root.tex; removed obsolete Isar_examples/Cantor.ML; renamed Real/Float.ML to Real/float.ML;
2006-09-28 paulson 2006-09-28 clearout of obsolete code
2006-09-19 wenzelm 2006-09-19 moved Import/susp.ML to Pure/General;
2006-09-19 haftmann 2006-09-19 added OperationalEquality.thy
2006-09-19 huffman 2006-09-19 add Real/RealVector.thy
2006-09-14 krauss 2006-09-14 updated makefile