src/Provers/splitter.ML
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago generic attributes;
2006-01-03 ago avoid hardwired Trueprop;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 ago accomodate simplified Thm.lift_rule;
2005-10-21 ago OldGoals;
2005-10-17 ago functor: no Simplifier argument;
2005-09-12 ago introduced new-style AList operations
2005-08-29 ago use AList operations;
2005-07-28 ago Sign.typ_match;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-01 ago removed obsolete sort 'logic';
2003-03-13 ago split_name no longer uses Sign.string_of_typ to encode types, since
2003-03-11 ago addsplits / delsplits no longer ignore type of constant.
2002-05-17 ago allowed more general split rules to cope with div/mod 2
2001-01-07 ago CHANGED_PROP;
2000-12-13 ago sar split method uses new gen_split_tac.
2000-11-07 ago Added type constraint in theorem "lift".
2000-11-06 ago Sign.typ_instance;
2000-09-19 ago tuned args;
2000-09-13 ago Args.addN, Args.delN;
2000-09-07 ago tuned msgs;
2000-09-02 ago "split": added "(asm)" option;
2000-08-28 ago added 'split' method;
2000-07-06 ago Now two split thms for same constant at different types is allowed.
2000-05-05 ago use Args.colon / Args.parens;
2000-03-31 ago use Attrib.add_del_args;
2000-03-15 ago made SML/XL happy;
2000-03-15 ago added attributes, method modifiers, theory setup;
1999-10-01 ago - Fixed bug in mk_split_pack which caused application of expansion theorem
1999-01-14 ago Fixed old bug: selection of constant to be split should depend not just on
1998-09-24 ago renamed mk_meta_eq to mk_eq
1998-09-08 ago added caveat; a real solution would be difficult
1998-08-12 ago the splitter is now defined as a functor
1998-05-14 ago extended addsplits and delsplits to handle also split rules for assumptions
1998-02-28 ago Little reorganization. Loop tactics have names now.
1998-01-07 ago adapted to new sort function;
1997-12-19 ago pasted old insertion sort (does not work with new sort function!)
1997-11-18 ago Fixed bug in inst_split.
1997-11-17 ago Tuned function mk_cntxt_splitthm.
1997-11-12 ago renamed split_prem_tac to split_asm_tac
1997-11-07 ago added split_prem_tac
1997-10-17 ago Added error messages.
1997-10-10 ago fixed dots;
1997-07-22 ago Removal of the tactical STATE
1996-11-28 ago Replaced map...~~ by ListPair.map
1996-11-01 ago Replaced min by Int.min
1996-05-06 ago Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
1996-04-25 ago Added functions mk_cntxt_splitthm and inst_split which instantiate
1995-04-16 ago Fixed bug.
1995-04-13 ago Completely rewrote split_tac. The old one failed in strange circumstances.
1995-03-08 ago Replaced read by read_cterm.
1995-03-03 ago replaced Pure by ProtoPure
1994-01-18 ago Updated refs to old Sign functions
1993-09-16 ago added header
1993-09-16 ago Initial revision