| changeset 11181 | d04f57b91166 |
| parent 11164 | 03f5dc539fd9 |
| child 11324 | 82406bd816a5 |
--- a/src/HOL/NatArith.thy Fri Feb 23 16:31:18 2001 +0100 +++ b/src/HOL/NatArith.thy Fri Feb 23 16:31:21 2001 +0100 @@ -18,7 +18,7 @@ val nat_diff_split = thm "nat_diff_split"; (* TODO: use this for force_tac in Provers/clasip.ML *) -fun add_arith cs = cs addaltern ("arith_tac", arith_tac); +fun add_arith cs = cs addafter ("arith_tac", arith_tac); *} lemmas [arith_split] = nat_diff_split split_min split_max