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
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.
1995-04-13 nipkow 1995-04-13 Completely rewrote split_tac. The old one failed in strange circumstances.
1995-03-08 nipkow 1995-03-08 Replaced read by read_cterm.
1995-03-03 clasohm 1995-03-03 replaced Pure by ProtoPure
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1993-09-16 nipkow 1993-09-16 added header
1993-09-16 clasohm 1993-09-16 Initial revision