src/Provers/splitter.ML
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-07-27 webertj 2006-07-27 type annotation added to make SML/NJ happy
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-02-10 wenzelm 2006-02-10 Args/Attrib syntax: Context.generic;
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;
2006-01-03 wenzelm 2006-01-03 avoid hardwired Trueprop; local proof: static refererence to Pure.thy;
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-17 wenzelm 2005-10-17 functor: no Simplifier argument; change_simpset;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-07-28 wenzelm 2005-07-28 Sign.typ_match;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2003-03-13 berghofe 2003-03-13 split_name no longer uses Sign.string_of_typ to encode types, since this depends on the print mode and may lead to unpredictable results.
2003-03-11 berghofe 2003-03-11 addsplits / delsplits no longer ignore type of constant.
2002-05-17 nipkow 2002-05-17 allowed more general split rules to cope with div/mod 2
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2000-12-13 nipkow 2000-12-13 sar split method uses new gen_split_tac.
2000-11-07 berghofe 2000-11-07 Added type constraint in theorem "lift".
2000-11-06 wenzelm 2000-11-06 Sign.typ_instance;
2000-09-19 wenzelm 2000-09-19 tuned args;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-07 wenzelm 2000-09-07 tuned msgs;
2000-09-02 wenzelm 2000-09-02 "split": added "(asm)" option;
2000-08-28 wenzelm 2000-08-28 added 'split' method;
2000-07-06 nipkow 2000-07-06 Now two split thms for same constant at different types is allowed.
2000-05-05 wenzelm 2000-05-05 use Args.colon / Args.parens;
2000-03-31 wenzelm 2000-03-31 use Attrib.add_del_args;
2000-03-15 wenzelm 2000-03-15 made SML/XL happy;
2000-03-15 wenzelm 2000-03-15 added attributes, method modifiers, theory setup;
1999-10-01 berghofe 1999-10-01 - Fixed bug in mk_split_pack which caused application of expansion theorem to fail because of typing reasons - Rewrote inst_lift and inst_split: now cterm_instantiate is used to instantiate theorems
1999-01-14 nipkow 1999-01-14 Fixed old bug: selection of constant to be split should depend not just on the name but also on the type.
1998-09-24 oheimb 1998-09-24 renamed mk_meta_eq to mk_eq
1998-09-08 oheimb 1998-09-08 added caveat; a real solution would be difficult
1998-08-12 oheimb 1998-08-12 the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset
1998-05-14 oheimb 1998-05-14 extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info
1998-02-28 nipkow 1998-02-28 Little reorganization. Loop tactics have names now.
1998-01-07 wenzelm 1998-01-07 adapted to new sort function;
1997-12-19 wenzelm 1997-12-19 pasted old insertion sort (does not work with new sort function!)
1997-11-18 berghofe 1997-11-18 Fixed bug in inst_split.
1997-11-17 berghofe 1997-11-17 Tuned function mk_cntxt_splitthm. Fixed bug which caused split_tac to fail when (Const ("splitconst", ...) $ ...) was of function type.
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac split_asm_tac: simplification, debugged first_prem_is_disj
1997-11-07 oheimb 1997-11-07 added split_prem_tac
1997-10-17 nipkow 1997-10-17 Added error messages.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-11-01 paulson 1996-11-01 Replaced min by Int.min
1996-05-06 berghofe 1996-05-06 Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
1996-04-25 berghofe 1996-04-25 Added functions mk_cntxt_splitthm and inst_split which instantiate the split-rule before it is applied. Inserted some comments.
1995-04-16 nipkow 1995-04-16 Fixed bug.