equal
deleted
inserted
replaced
13 (rare) case use delSWrapper "split_all_tac" addSbefore |
13 (rare) case use delSWrapper "split_all_tac" addSbefore |
14 ("unsafe_split_all_tac", unsafe_split_all_tac) |
14 ("unsafe_split_all_tac", unsafe_split_all_tac) |
15 |
15 |
16 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS |
16 * HOL: added safe wrapper "split_conv_tac" to claset. EXISTING PROOFS |
17 MAY FAIL; |
17 MAY FAIL; |
|
18 |
|
19 * Classical reasoner: renamed addaltern to addafter, addSaltern to addSafter |
18 |
20 |
19 * HOL: introduced f^n = f o ... o f |
21 * HOL: introduced f^n = f o ... o f |
20 WARNING: due to the limits of Isabelle's type classes, ^ on functions and |
22 WARNING: due to the limits of Isabelle's type classes, ^ on functions and |
21 relations has too general a domain, namely ('a * 'b)set and 'a => 'b. |
23 relations has too general a domain, namely ('a * 'b)set and 'a => 'b. |
22 This means that it may be necessary to attach explicit type constraints. |
24 This means that it may be necessary to attach explicit type constraints. |