src/Pure/Thy/thm_database.ML
1998-08-20 paulson 1998-08-20 Now qed_spec_mp respects locales, by calling ml_store_thm instead of bind_thm
1998-07-17 paulson 1998-07-17 added comments
1998-06-29 wenzelm 1998-06-29 use_text: verbose flag;
1998-06-15 wenzelm 1998-06-15 use_text replaces use_strings;
1998-01-09 wenzelm 1998-01-09 thm_ord;
1998-01-08 wenzelm 1998-01-08 fixed thm_less;
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-26 wenzelm 1997-11-26 fixed type of thms_containing;
1997-10-30 wenzelm 1997-10-30 tuned;
1997-10-28 wenzelm 1997-10-28 restructured -- uses PureThy storage facilities;
1997-10-24 wenzelm 1997-10-24 ProtoPure.flexpair_def;
1997-10-23 wenzelm 1997-10-23 tuned;
1997-08-06 wenzelm 1997-08-06 renamed use_string to use_strings;
1997-08-06 wenzelm 1997-08-06 tuned names;
1997-08-06 berghofe 1997-08-06 Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
1996-11-01 paulson 1996-11-01 Replaced "sum" (only usage?) by foldl op+
1996-05-17 nipkow 1996-05-17 Added missing default clause | top_const _ = None;
1996-04-09 berghofe 1996-04-09 select_match now sorts list of matching theorems according to the number of premises and size of the required substitution
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1995-10-25 clasohm 1995-10-25 removed "duplicate" warning from store_thm_db; changed place where store_thm_db is called for a theory's axioms
1995-10-06 clasohm 1995-10-06 changed some comments
1995-10-04 clasohm 1995-10-04 added removal of theorems if theory is to be reloaded; changed functions for local simpsets
1995-09-01 clasohm 1995-09-01 fixed bug: duplicate "duplicate" warnings
1995-09-01 clasohm 1995-09-01 added cleanup of global simpset to thy_read; replaced error by warning for duplicate names in theorem database
1995-08-30 clasohm 1995-08-30 added check for duplicate theorems in theorem database; changed warnings and error messages in thy_read to distinguish between theorems in theor_y_ database and in theor_em_ database
1995-08-18 nipkow 1995-08-18 fixed bug in findI removed duplicates in findEs
1995-08-07 nipkow 1995-08-07 Added findI, findEs, and findE.
1995-06-01 clasohm 1995-06-01 commented thms_unifying_with out; placed thm_db into signature again; placed structures ThmDB and Readthy into Pure again; changed init_thy_reader so that thm_db and loaded_thys are preserved (necessary e.g. for ZF)
1995-05-30 clasohm 1995-05-30 removed thm_num and thm_db from signature
1995-05-30 clasohm 1995-05-30 fixed bug in thms_containing; changed error/warning messages; added thms_resolving_with
1995-05-29 clasohm 1995-05-29 changed error message in thms_containing
1995-05-29 clasohm 1995-05-29 added theorem database which contains axioms and theorems indexed by the constants they contain