src/Pure/Isar/induct_attrib.ML
2007-05-07 ago simplified DataFun interfaces;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-08 ago introduced gen_distinct in place of distinct
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-10 ago generic data and attributes;
2005-11-22 ago find_xxxS: term instead of thm;
2005-11-19 ago added coinduct attribute;
2005-08-29 ago use AList operations;
2005-07-13 ago (intermediate commit)
2005-06-17 ago accomodate change of TheoryDataFun;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-03 ago Move towards standard functions.
2004-06-21 ago Merged in license change from Isabelle2004
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
2001-12-05 ago simplified NetRules;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-09 ago theory data: finish method;
2001-11-08 ago make SML/XL of NJ happy;
2001-11-05 ago pretty/print functions with context;
2001-10-16 ago allow empty set/type name;
2001-10-15 ago tuned NetRules;
2001-10-12 ago removed get_cases, get_induct;
2001-10-04 ago tuned print operation;
2001-10-03 ago Isar/induct_attrib.ML;
2001-10-03 ago moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;