src/ZF/Tools/induct_tacs.ML
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-27 wenzelm 2009-07-27 moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
2009-03-15 wenzelm 2009-03-15 simplified method setup;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 proper context for tactics derived from res_inst_tac;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-10 wenzelm 2008-04-10 tuned;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-09-26 wenzelm 2007-09-26 Attrib.eval_thms;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-01-19 wenzelm 2007-01-19 moved parts of OuterParse to SpecParse;
2006-11-14 wenzelm 2006-11-14 incorporated IsarThy into IsarCmd;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Eliminated hack for deleting leading question mark from induction variable name.
2003-08-19 paulson 2003-08-19 new case_tac
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-15 wenzelm 2001-11-15 Isar version of 'rep_datatype';
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
1999-07-10 wenzelm 1999-07-10 pass exn;
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-06 paulson 1999-01-06 induct_tac and exhaust_tac