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