author | paulson |
Fri, 12 May 2000 15:18:55 +0200 | |
changeset 8868 | 851693e780d6 |
parent 8867 | 06dcd62f65ad |
child 8869 | 9ba7ef8a765b |
--- a/src/HOL/UNITY/Token.ML Fri May 12 15:15:27 2000 +0200 +++ b/src/HOL/UNITY/Token.ML Fri May 12 15:18:55 2000 +0200 @@ -52,7 +52,7 @@ "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq])); by (auto_tac (claset(), - simpset() addsplits [nat_diff_split'] + simpset() addsplits [nat_diff_split] addsimps [linorder_neq_iff, mod_geq])); qed "nodeOrder_eq";