src/HOL/IsaMakefile
2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-11-29 paulson 2000-11-29 new simproc file cancel_numeral_factor.ML
2000-11-17 wenzelm 2000-11-17 Library/Ring_and_Field.thy;
2000-11-10 wenzelm 2000-11-10 proper theory context for mesontest2;
2000-10-30 wenzelm 2000-10-30 added ex/PER.thy;
2000-10-26 nipkow 2000-10-26 *** empty log message ***
2000-10-25 wenzelm 2000-10-25 "List prefixes" library theory (replaces old Lex/Prefix);
2000-10-19 wenzelm 2000-10-19 added Tools/induct_attrib.ML;
2000-10-18 wenzelm 2000-10-18 removed Library/Accessible_Part.ML;
2000-10-18 wenzelm 2000-10-18 added HOL/Library, rearranged several files;
2000-10-13 nipkow 2000-10-13 *** empty log message ***
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;