src/HOL/IsaMakefile
1999-09-22 wenzelm 1999-09-22 proper theory setup for Real/ex/BinEx;
1999-09-10 wenzelm 1999-09-10 The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);
1999-09-08 paulson 1999-09-08 new example HOL/UNITY/TimerArray
1999-09-02 wenzelm 1999-09-02 renamed NatSum to Summation;
1999-09-01 wenzelm 1999-09-01 Isar_examples/MultisetOrder.thy;
1999-08-31 paulson 1999-08-31 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration for the overloading of <, while .ML file gets proofs about renaming constants
1999-08-30 wenzelm 1999-08-30 clean: include HOL-Real-ex;
1999-08-30 paulson 1999-08-30 make it actually RUN the real examples
1999-08-30 paulson 1999-08-30 new directory HOL/Real/ex of real examples
1999-08-29 wenzelm 1999-08-29 added Isar_examples/MutilatedCheckerboard.thy;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-24 wenzelm 1999-08-24 Real/Real.thy main entry point;
1999-08-20 wenzelm 1999-08-20 eliminated HOL-AxClasses target;
1999-08-20 paulson 1999-08-20 new theories RealBin, RealInt, RealPow
1999-08-17 wenzelm 1999-08-17 tuned;
1999-08-16 paulson 1999-08-16 new theory Real/Hyperreal/HyperDef and file fuf.ML
1999-08-06 paulson 1999-08-06 new theory UNITY/Lift_prog
1999-08-06 paulson 1999-08-06 new theory ex/svc_test.thy
1999-08-03 paulson 1999-08-03 new examples file for SVC
1999-08-02 paulson 1999-08-02 new files for the SVC link-up
1999-07-28 wenzelm 1999-07-28 HOL-Real target now builds an actual image;
1999-07-26 paulson 1999-07-26 HOL/ex/Tarski: new example by Florian Kammueller
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals
1999-07-08 paulson 1999-07-08 new files IntDiv.{thy,ML}
1999-07-06 wenzelm 1999-07-06 added Numeral.thy, Tools/numeral_syntax.ML;
1999-07-01 wenzelm 1999-07-01 Isar_examples/KnasterTarski.thy;
1999-06-11 paulson 1999-06-11 new UNITY files
1999-06-04 wenzelm 1999-06-04 Calculation.thy: Setup transitivity rules for calculational proofs.
1999-06-04 wenzelm 1999-06-04 added Isar_examples/Group.thy;
1999-05-26 wenzelm 1999-05-26 ex/Points Isar'ized;
1999-05-26 paulson 1999-05-26 new theories Follows and ListOrder
1999-04-28 paulson 1999-04-28 eliminated theory UNITY/Traces
1999-04-27 wenzelm 1999-04-27 added Isar_examples/NatSum.thy;
1999-04-27 wenzelm 1999-04-27 added Isar_examples/Cantor.ML;
1999-04-23 paulson 1999-04-23 Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
1999-04-22 wenzelm 1999-04-22 tuned;
1999-04-22 mueller 1999-04-22 deleted some old examples in Modelcheck;
1999-04-16 wenzelm 1999-04-16 added Isar_examples;
1999-04-16 wenzelm 1999-04-16 added Tools/induct_method.ML;
1999-04-14 wenzelm 1999-04-14 Tools/inductive_package.ML;
1999-03-18 paulson 1999-03-18 added new theory Yahalom_Bad
1999-03-03 paulson 1999-03-03 added UNITY/Extend
1999-02-08 wenzelm 1999-02-08 updated TLA;
1999-02-05 wenzelm 1999-02-05 Hyperreal made part of Real;
1999-01-04 nipkow 1999-01-04 Version 1.0 of linear nat arithmetic.
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-11-27 paulson 1998-11-27 added Real/Hyperreal
1998-11-17 paulson 1998-11-17 new theory UNITY/PPROD
1998-10-23 narasche 1998-10-23 ex/Points added
1998-10-23 berghofe 1998-10-23 Directory Induct: Added new theory ABexp, removed obsolete theory Simult.
1998-10-21 wenzelm 1998-10-21 tuned;
1998-10-20 wenzelm 1998-10-20 split_paired_all.ML;
1998-10-13 paulson 1998-10-13 Addition of HOL/UNITY/Client
1998-10-09 nipkow 1998-10-09 added Induct/Multiset*
1998-10-07 paulson 1998-10-07 new files UNITY/Comp.{thy,ML}
1998-10-06 nipkow 1998-10-06 Merges FoldSet into Finite
1998-10-02 paulson 1998-10-02 new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
1998-09-25 paulson 1998-09-25 Renaming of Integ/Integ.* to Integ/Int.*
1998-09-18 paulson 1998-09-18 new files in Integ
1998-09-07 paulson 1998-09-07 New UNITY theory, the N-S protocol