src/HOL/thy_data.ML
1997-12-28 wenzelm 1997-12-28 Symtab.empty;
1997-12-19 narasche 1997-12-19 remove signatrue from records
1997-12-01 narasche 1997-12-01 args for record data
1997-11-20 wenzelm 1997-11-20 adapted print methods;
1997-11-05 wenzelm 1997-11-05 tuned record_info;
1997-11-04 wenzelm 1997-11-04 tuned 'records' stuff;
1997-11-04 narasche 1997-11-04 data kinds 'datatypes', data kinds 'records' added
1997-11-03 wenzelm 1997-11-03 datatypes;
1997-11-03 wenzelm 1997-11-03 HOL theory data.
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-07-09 wenzelm 1997-07-09 removed obsolete init_pps and init_thy_reader;
1997-05-22 nipkow 1997-05-22 exhaust_tac can now deal with whole terms rather than just variables.
1997-05-22 nipkow 1997-05-22 Added exhaustion thm and exhaust_tac for each datatype.
1997-05-21 nipkow 1997-05-21 Replaced Konrad's own add_term_names by the predefined one. Replaced fn Free x => x by dest_Free.
1997-04-24 nipkow 1997-04-24 Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...
1997-01-29 paulson 1997-01-29 Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work properly in children databases
1996-05-07 berghofe 1996-05-07 Added function claset_of.
1996-04-19 clasohm 1996-04-19 added Konrad's code for the datatype package
1996-04-12 clasohm 1996-04-12 changed first parameter of add_thydata and get_thydata
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-29 clasohm 1996-01-29 changed the way simpsets and information about datatypes are stored