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);