src/Provers/splitter.ML
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