src/HOL/IsaMakefile
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
1998-05-11 nipkow 1998-05-11 Lex
1998-05-05 paulson 1998-05-05 New syntax for function update; moved to main HOL directory
1998-04-29 wenzelm 1998-04-29 removed typedef.ML, record.ML; added Tools/typedef_package.ML, Tools/record_package.ML, Record.thy;
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-03 paulson 1998-04-03 New target HOL-UNITY
1998-03-11 nipkow 1998-03-11 More Lex.
1998-03-09 wenzelm 1998-03-09 tuned;
1998-02-26 paulson 1998-02-26 New theory, Vimage
1998-01-07 wenzelm 1998-01-07 improved targets; fixed dependencies on parent logics;
1997-12-19 wenzelm 1997-12-19 added record.ML;
1997-12-19 wenzelm 1997-12-19 log files; 'clean' target;
1997-11-26 wenzelm 1997-11-26 tuned;
1997-11-21 oheimb 1997-11-21 corrected INDUCT_FILES
1997-11-03 wenzelm 1997-11-03 added thy_data.ML;
1997-10-24 nipkow 1997-10-24 Added the new theory Map.
1997-10-09 wenzelm 1997-10-09 added TLA stuff;
1997-08-06 berghofe 1997-08-06 Removed references to "thy_data.ML".
1997-07-22 paulson 1997-07-22 Fixed the spelling of AUTH_NAMES--it could not have worked before\!
1997-07-07 wenzelm 1997-07-07 eliminated chmod -w;
1997-07-01 paulson 1997-07-01 New theory TLS
1997-06-06 paulson 1997-06-06 New example theory: Recdef
1997-06-03 paulson 1997-06-03 New theory "Power" of exponentiation (and binomial coefficients)