unsymbolize;

--- a/src/HOL/Integ/IntDiv.ML	Tue Oct 03 18:44:19 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Tue Oct 03 18:45:36 2000 +0200
@@ -329,7 +329,7 @@
 val lemma = result();
 
 Goal "b ~= (#0::int) \
-\     \\<Longrightarrow> (-a) div b = \
+\     ==> (-a) div b = \
 \         (if a mod b = #0 then - (a div b) else  - (a div b) - #1)";
 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
 qed "zdiv_zminus1_eq_if";
@@ -350,7 +350,7 @@
 qed "zmod_zminus2";
 
 Goal "b ~= (#0::int) \
-\     \\<Longrightarrow> a div (-b) = \
+\     ==> a div (-b) = \
 \         (if a mod b = #0 then - (a div b) else  - (a div b) - #1)";
 by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); 
 qed "zdiv_zminus2_eq_if";

--- a/src/HOL/Integ/int_arith2.ML	Tue Oct 03 18:44:19 2000 +0200
+++ b/src/HOL/Integ/int_arith2.ML	Tue Oct 03 18:45:36 2000 +0200
@@ -57,7 +57,7 @@
 by (Simp_tac 1);
 qed "nat_less_iff";
 
-Goal "(int m = z) = (m = nat z & #0 \\<le> z)";
+Goal "(int m = z) = (m = nat z & #0 <= z)";
 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2]));  
 qed "int_eq_iff";