src/HOL/IsaMakefile
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
1998-09-01 paulson 1998-09-01 new theory Induct/FoldSet
1998-08-24 wenzelm 1998-08-24 added Antiquote example;
1998-08-21 paulson 1998-08-21 New UNITY files
1998-08-17 nipkow 1998-08-17 Additions to Lex.
1998-08-12 oheimb 1998-08-12 cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML
1998-08-06 nipkow 1998-08-06 New lemmas in List and Lambda in IsaMakefile
1998-08-04 wenzelm 1998-08-04 added LocaleGroup, PiSets examples;
1998-07-31 paulson 1998-07-31 Removed HOL/IMP/Com.ML because it contained only an "open" declaration
1998-07-24 wenzelm 1998-07-24 added ex/MonoidGroups (record example); moved Bin and String examples to ex;
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-03 wenzelm 1998-07-03 stepping stones: Recdef, Main; String now part of main HOL;
1998-07-02 wenzelm 1998-07-02 fixed Integ;
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real
1998-06-11 nipkow 1998-06-11 removed rel.ML