src/HOL/IsaMakefile
2001-09-27 wenzelm ex/Hilbert_Classical.thy ex/document/root.tex;
2001-08-31 wenzelm HOL-Real-Hyperreal made a plain session (no longer an image);
2001-08-31 berghofe Added new files for code generator.
2001-07-25 paulson partial restructuring to reduce dependence on Axiom of Choice
2001-07-23 paulson new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-03 wenzelm Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
2001-07-03 paulson Locale-based group theory proofs
2001-06-16 oheimb added NanoJava
2001-06-10 paulson new GroupTheory example, e.g. the Sylow theorem (preliminary version)
2001-06-09 paulson moved Primes.thy from NumberTheory to Library
2001-06-08 nipkow Removed BCV
2001-05-31 wenzelm added HOL-CTL;
2001-05-31 oheimb added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-08 paulson conversion of Auth/TLS to Isar script
2001-04-24 paulson (rough) conversion of Auth/Recur to Isar format
2001-04-12 paulson converted many HOL/Auth theories to Isar scripts
2001-03-28 nipkow MicroJava/BV dependencies incomplete
2001-03-23 nipkow added one point simprocs for bounded quantifiers
2001-03-05 paulson reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-02 paulson conversion of Message.thy to Isar format
2001-02-15 oheimb Ord.thy/.ML converted to Isar
2001-02-13 paulson partial conversion to Isar script style in HOL/Auth removes some .ML files
2001-02-09 kleing removed MicroJava/Digest.thy
2001-02-04 wenzelm HOL-NumberTheory: converted to new-style format and proper document setup;
2001-02-03 wenzelm Induct: converted some theories to new-style format;
2001-02-01 oheimb converted to Isar, simplifying recursion on class hierarchy
2001-02-01 wenzelm converted to new-style theories;
2001-01-28 nipkow fixed set comprehension print translation
2001-01-25 wenzelm tuned;
2001-01-25 wenzelm Transitive_Closure turned into new-style theory;
2001-01-23 wenzelm added HOL-Unix example;
2001-01-19 wenzelm added Library/Ring_and_Field_Example.thy;
2001-01-19 wenzelm added HOL/Library/Nested_Environment.thy;
2001-01-16 kleing removed obsolete MicroJava/JVM/Store.thy
2001-01-15 wenzelm removed ex/StringEx.ML;
2001-01-12 wenzelm added Induct/Sigma_Algebra.thy;
2001-01-07 wenzelm removed MicroJava/BV/Convert.thy;
2001-01-05 paulson new UNITY examples by Sidi Ehmety
2001-01-03 wenzelm TFL: renamed .sml to .ML;
2001-01-01 paulson put in some missing Hyperreal files
2000-12-30 paulson separation of HOL-Hyperreal from HOL-Real
2000-12-23 wenzelm Tools/string_syntax.ML;
2000-12-21 nipkow *** empty log message ***
2000-12-19 paulson new file extract_common_term.ML for the cancel-factor simprocs
2000-12-16 wenzelm tuned HOL/Real/HahnBanach;
2000-12-06 wenzelm added Library/Rational_Numbers.thy;
2000-12-01 nipkow Linear arithmetic now copes with mixed nat/int formulae.
2000-11-29 paulson new simproc file cancel_numeral_factor.ML
2000-11-17 wenzelm Library/Ring_and_Field.thy;
2000-11-10 wenzelm proper theory context for mesontest2;
2000-10-30 wenzelm added ex/PER.thy;
2000-10-26 nipkow *** empty log message ***
2000-10-25 wenzelm "List prefixes" library theory (replaces old Lex/Prefix);
2000-10-19 wenzelm added Tools/induct_attrib.ML;
2000-10-18 wenzelm removed Library/Accessible_Part.ML;
2000-10-18 wenzelm added HOL/Library, rearranged several files;
2000-10-13 nipkow *** empty log message ***
2000-10-12 nipkow *** empty log message ***
2000-10-05 wenzelm * HOL/Lattice: fundamental concepts of lattice theory and order structures;
2000-10-03 wenzelm added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
less more (0) -100 -60 tip