src/HOL/Hoare/Arith2.ML

--- a/src/HOL/Hoare/Arith2.ML	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Fri Oct 05 21:52:39 2001 +0200
@@ -63,7 +63,7 @@
 
 (*** 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";