equal
deleted
inserted
replaced
1 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
2 ============================================== |
|
3 |
|
4 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL |
3 |
5 |
4 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this |
6 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this |
5 (rare) case use delSWrapper "split_all_tac" addSbefore |
7 (rare) case use delSWrapper "split_all_tac" addSbefore |
6 ("unsafe_split_all_tac", unsafe_split_all_tac) |
8 ("unsafe_split_all_tac", unsafe_split_all_tac) |
7 |
9 |