# HG changeset patch
# User paulson
# Date 957446137 -7200
# Node ID 50b650d1964106cbe67a0b7e0bd6d565bc392eac
# Parent  c4aaa5936e0c2c07932442f93a20f4e5693d8e7f
changed 2 to #2

diff -r c4aaa5936e0c -r 50b650d19641 src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Thu May 04 15:15:37 2000 +0200
@@ -63,10 +63,8 @@
 
 (*** pow ***)
 
-Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
-by (subgoal_tac "n*n=n^2" 1);
-by (etac ssubst 1 THEN stac (power_mult RS sym) 1);
-by (stac mult_div_cancel 1);
-by (ALLGOALS Asm_simp_tac);
+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];
diff -r c4aaa5936e0c -r 50b650d19641 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Thu May 04 15:15:37 2000 +0200
@@ -6,7 +6,7 @@
 More arithmetic.  Much of this duplicates ex/Primes.
 *)
 
-Arith2 = Power +
+Arith2 = Main +
 
 constdefs
   cd      :: [nat, nat, nat] => bool
diff -r c4aaa5936e0c -r 50b650d19641 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/Hoare/Examples.ML	Thu May 04 15:15:37 2000 +0200
@@ -43,17 +43,16 @@
 \ c := 1; \
 \ WHILE b ~= 0 \
 \ INV {A^B = c * a^b} \
-\ DO  WHILE b mod 2 = 0 \
+\ DO  WHILE b mod #2 = 0 \
 \     INV {A^B = c * a^b} \
-\     DO  a := a*a; b := b div 2 OD; \
+\     DO  a := a*a; b := b div #2 OD; \
 \     c := c*a; b := b-1 \
 \ OD \
 \ {c = A^B}";
 by (hoare_tac (Asm_full_simp_tac) 1);
 by (case_tac "b" 1);
-by (hyp_subst_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
-by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
+by (Asm_simp_tac 1);
 qed "power_by_mult";
 
 (** Factorial **)
diff -r c4aaa5936e0c -r 50b650d19641 src/HOL/IMPP/EvenOdd.ML
--- a/src/HOL/IMPP/EvenOdd.ML	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/IMPP/EvenOdd.ML	Thu May 04 15:15:37 2000 +0200
@@ -19,7 +19,7 @@
 Addsimps [not_even_1];
 
 Goalw [even_def] "even (Suc (Suc n)) = even n";
-by (subgoal_tac "Suc (Suc n) = n+2" 1);
+by (subgoal_tac "Suc (Suc n) = n+#2" 1);
 by  (Simp_tac 2);
 be ssubst 1;
 br dvd_reduce 1;
diff -r c4aaa5936e0c -r 50b650d19641 src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy	Thu May 04 15:15:37 2000 +0200
@@ -9,7 +9,7 @@
 EvenOdd = Misc +
 
 constdefs even :: nat => bool
-  "even n == 2 dvd n"
+  "even n == #2 dvd n"
 
 consts
   Even, Odd :: pname
diff -r c4aaa5936e0c -r 50b650d19641 src/HOL/Quot/FRACT.ML
--- a/src/HOL/Quot/FRACT.ML	Thu May 04 15:14:56 2000 +0200
+++ b/src/HOL/Quot/FRACT.ML	Thu May 04 15:15:37 2000 +0200
@@ -11,7 +11,7 @@
 qed "inst_NP_per";
 
 
-Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
+Goalw [half_def] "half = <[abs_NP(n,#2*n)]>";
 by (rtac per_class_eqI 1);
 by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
 qed "test";