nat_diff_split' now called nat_diff_split
authorpaulson
Fri, 12 May 2000 15:18:55 +0200
changeset 8868 851693e780d6
parent 8867 06dcd62f65ad
child 8869 9ba7ef8a765b
nat_diff_split' now called nat_diff_split
src/HOL/UNITY/Token.ML
--- 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";