unsymbolize;

--- a/src/ZF/Integ/Bin.ML	Thu Dec 07 22:35:25 2000 +0100
+++ b/src/ZF/Integ/Bin.ML	Fri Dec 08 00:04:34 2000 +0100
@@ -532,7 +532,7 @@
 by Auto_tac;  
 qed "nat_le_int0";
 
-Goal "$# n = #0 \\<Longrightarrow> natify(n) = 0";
+Goal "$# n = #0 ==> natify(n) = 0";
 by (rtac not_znegative_imp_zero 1);
 by Auto_tac;  
 qed "int_of_eq_0_imp_natify_eq_0";
@@ -545,7 +545,7 @@
 by (blast_tac (claset() addIs [int_of_eq_0_imp_natify_eq_0, sym]) 1); 
 qed "nat_of_zminus_int_of";
 
-Goal "#0 $<= z \\<Longrightarrow> $# nat_of(z) = intify(z)";
+Goal "#0 $<= z ==> $# nat_of(z) = intify(z)";
 by (rtac not_zneg_nat_of_intify 1);
 by (asm_simp_tac (simpset() addsimps [znegative_iff_zless_0, 
                                       not_zless_iff_zle]) 1); 

--- a/src/ZF/Integ/IntDiv.ML	Thu Dec 07 22:35:25 2000 +0100
+++ b/src/ZF/Integ/IntDiv.ML	Fri Dec 08 00:04:34 2000 +0100
@@ -383,8 +383,8 @@
 Addsimps [adjust_eq];
 
 
-Goal "\\<lbrakk>#0 $< b; \\<not> a $< b\\<rbrakk>   \
-\     \\<Longrightarrow> nat_of(a $- #2 $\\<times> b $+ #1) < nat_of(a $- b $+ #1)";
+Goal "[| #0 $< b; \\<not> a $< b |]   \
+\     ==> nat_of(a $- #2 $\\<times> b $+ #1) < nat_of(a $- b $+ #1)";
 by (simp_tac (simpset() addsimps [zless_nat_conj]) 1);
 by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle,
                        zless_add1_iff_zle]@zcompare_rls) 1); 
@@ -404,7 +404,7 @@
 Goal "[| !!a b. [| a: int; b: int; \
 \                  ~ (a $< b | b $<= #0) --> P(<a, #2 $* b>) |] \
 \               ==> P(<a,b>) |] \
-\     ==> <u,v>: int*int \\<longrightarrow> P(<u,v>)"; 
+\     ==> <u,v>: int*int --> P(<u,v>)"; 
 by (res_inst_tac [("a","<u,v>")] wf_induct 1);
 by (res_inst_tac [("A","int*int"), ("f","%<a,b>.nat_of (a $- b $+ #1)")] 
                  wf_measure 1);