doc-src/AxClass/Nat/NatClass.ML
changeset 25985 8d69087f6a4b
parent 24584 01e83ffa6c54
--- a/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 17:08:43 2008 +0100
+++ b/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 20:01:37 2008 +0100
@@ -34,7 +34,7 @@
 back();
 back();
 
-Goalw [add_def] "\\<zero>+n = n";
+Goalw [add_def] "\<zero>+n = n";
 by (rtac rec_0 1);
 qed "add_0";
 
@@ -50,7 +50,7 @@
 by (Asm_simp_tac 1);
 qed "add_assoc";
 
-Goal "m+\\<zero> = m";
+Goal "m+\<zero> = m";
 by (res_inst_tac [("n","m")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);