equal
deleted
inserted
replaced
14 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL |
14 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS MAY FAIL |
15 |
15 |
16 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this |
16 * HOL: made split_all_tac safe. EXISTING PROOFS MAY FAIL OR LOOP, so in this |
17 (rare) case use delSWrapper "split_all_tac" addSbefore |
17 (rare) case use delSWrapper "split_all_tac" addSbefore |
18 ("unsafe_split_all_tac", unsafe_split_all_tac) |
18 ("unsafe_split_all_tac", unsafe_split_all_tac) |
|
19 |
|
20 * HOL/GroupTheory: group theory examples including Sylow's theorem, by Florian |
|
21 Kammueller; |
19 |
22 |
20 * ZF: the integer library now covers quotients and remainders, with many laws |
23 * ZF: the integer library now covers quotients and remainders, with many laws |
21 relating division to addition, multiplication, etc.; |
24 relating division to addition, multiplication, etc.; |
22 |
25 |
23 |
26 |