src/HOL/Hoare/Arith2.ML

 qed "gcd_diff_r";
 
 
 (*** pow ***)
 
-Goal "m mod #2 = 0 ==> ((n::nat)*n)^(m div #2) = n^m";
+Goal "m mod # 2 = 0 ==> ((n::nat)*n)^(m div # 2) = n^m";
 by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
 				      mult_div_cancel]) 1);
 qed "sq_pow_div2";
 Addsimps [sq_pow_div2];