src/HOL/ex/Primes.ML

 (* Property 1: egcd m n divides m and n *)
 
 goal thy "ALL m. (egcd m n dvd m) & (egcd m n dvd n)";
 by (res_inst_tac [("n","n")] less_induct 1);
 by (rtac allI 1);
-by (excluded_middle_tac "n=0" 1);
+by (case_tac "n=0" 1);
 (* case n = 0 *)
-by (Asm_simp_tac 2);
+by (Asm_simp_tac 1);
 (* case n > 0 *)
 by (asm_full_simp_tac (!simpset addsimps [zero_less_eq RS sym]) 1);
 by (eres_inst_tac [("x","m mod n")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [mod_less_divisor]) 1);
 by (fast_tac (!claset addIs [gcd_ind]) 1);

 (* Property 2: for all m,n,f naturals, 
                if f divides m and f divides n then f divides egcd m n*)
 goal thy "!!k. ALL m. (f dvd m) & (f dvd k) --> f dvd egcd m k";
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rtac allI 1);
-by (excluded_middle_tac "n=0" 1);
+by (case_tac "n=0" 1);
 (* case n = 0 *)
-by (Asm_simp_tac 2);
+by (Asm_simp_tac 1);
 (* case n > 0 *)
 by (Step_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [zero_less_eq RS sym]) 1);
 by (eres_inst_tac [("x","m mod n")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [mod_less_divisor]) 1);