src/HOL/IsaMakefile
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-06 wenzelm 2000-10-06 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
2000-10-03 wenzelm 2000-10-03 added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
2000-10-03 wenzelm 2000-10-03 reorganized AxClasses;
2000-09-27 wenzelm 2000-09-27 proper Hyperreal setup;
2000-09-22 kleing 2000-09-22 removed JVM/Store.ML, added theorem Digest in MicroJava
2000-09-21 wenzelm 2000-09-21 renamed HOL/ex/Points to HOL/ex/Records;
2000-09-13 paulson 2000-09-13 moved Primes, Fib, Factorization to HOL/NumberTheory
2000-09-12 wenzelm 2000-09-12 added MicroJava/document/root.bib;
2000-09-07 wenzelm 2000-09-07 added Provers/rulify.ML;
2000-09-05 wenzelm 2000-09-05 improved meson setup;
2000-09-05 paulson 2000-09-05 meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
2000-09-04 paulson 2000-09-04 Converting HOL/ex/Primes.thy to new style, removing Primes.ML
2000-09-04 nipkow 2000-09-04 BCV
2000-09-02 wenzelm 2000-09-02 Lambda/document/root.tex;
2000-09-02 wenzelm 2000-09-02 HOL/Lambda: converted into new-style theory and document;
2000-09-01 wenzelm 2000-09-01 converted Lambda scripts;
2000-08-31 wenzelm 2000-08-31 ported HOL/Lambda/ListBeta;
2000-08-30 kleing 2000-08-30 MicroJava changed (all of BV -> Isar)
2000-08-29 wenzelm 2000-08-29 Lambda/InductTermi made new-style theory; tuned;
2000-08-18 wenzelm 2000-08-18 Main now new-style theory; added Main.ML for compatibility;
2000-08-17 wenzelm 2000-08-17 removed Lambda/Type.ML;
2000-08-14 kleing 2000-08-14 added MicroJava/BV/StepMono.thy, converted MicroJava/BV/Convert.thy to Isar
2000-08-07 kleing 2000-08-07 MicroJava structure changed
2000-08-03 wenzelm 2000-08-03 tuned TLA;
2000-08-03 paulson 2000-08-03 new files Integ/IntPower.{thy.ML}; tidied
2000-07-31 wenzelm 2000-07-31 tuned;
2000-07-31 nipkow 2000-07-31 Removed Quot
2000-07-27 wenzelm 2000-07-27 added theory While;
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
2000-07-18 kleing 2000-07-18 MicroJava structure changed
2000-07-16 wenzelm 2000-07-16 added ex/Tuple.thy;
2000-07-14 oheimb 2000-07-14 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
2000-07-07 oheimb 2000-07-07 added IMP/Examples.ML dependence
2000-07-05 oheimb 2000-07-05 disambiguated := ; added Examples (factorial)
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
2000-06-28 paulson 2000-06-28 new file Provers/make_elim.ML
2000-06-23 berghofe 2000-06-23 Added new theory Lambda/Type.
2000-06-21 wenzelm 2000-06-21 fixed deps;
2000-06-07 paulson 2000-06-07 Real/simproc.ML now removed
2000-06-02 oheimb 2000-06-02 added HOL/Prolog
2000-05-24 paulson 2000-05-24 Adding SetInterval, deleting UNITY/LessThan
2000-05-24 paulson 2000-05-24 restored NatSum.thy
2000-05-23 paulson 2000-05-23 IntRingDefs is now redundant
2000-05-23 paulson 2000-05-23 theory file NatSum.thy no longer needed new files for the Allocator: AllocBase.{thy,ML}
2000-05-22 wenzelm 2000-05-22 new Isar version of HOL-AxClasses-Tutorial;
2000-05-22 paulson 2000-05-22 new file Induct/MultisetOrder.thy
2000-05-15 paulson 2000-05-15 added the dummy theory Integ/NatSimprocs.thy
2000-05-08 wenzelm 2000-05-08 moved theory Sexp to Induct examples;
2000-05-05 wenzelm 2000-05-05 removed Pure/section_utils.ML;
2000-05-05 nipkow 2000-05-05 Added AVL
2000-05-02 paulson 2000-05-02 combine_numerals replaces both fold_Suc and combine_coeff
2000-04-21 paulson 2000-04-21 Provers/Arith/inverse_fold.ML is already obsolete Integ/NatSimprocs.ML added
2000-04-18 paulson 2000-04-18 new simprocs for numerals of type "nat"
2000-04-05 wenzelm 2000-04-05 added Isar_examples/NestedDatatype.thy;
2000-03-24 wenzelm 2000-03-24 added HOL/ex/Multiquote.thy;
2000-03-23 wenzelm 2000-03-23 ex/Antiquote.thy made new-style theory; removed ex/Antiquote.ML;
2000-03-23 paulson 2000-03-23 restored the MESON examples file HOL/ex/mesontest2.ML
2000-03-17 wenzelm 2000-03-17 fixed dep;
2000-03-16 wenzelm 2000-03-16 added HOL/PreLIst.thy;