Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 file | annotate | diff | comparison | revisions 
--- 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";
isabelle