# HG changeset patch
# User paulson
# Date 845631182 -7200
# Node ID 41a667d2c3faedc2d6edb71c5da6a9f26b0da74c
# Parent  5d44339454a4abd9d7908ec282c0d93a50128f24
Replaced excluded_middle_tac by case_tac

diff -r 5d44339454a4 -r 41a667d2c3fa src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Oct 18 11:32:38 1996 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Oct 18 11:33:02 1996 +0200
@@ -372,7 +372,8 @@
 by (etac analz.induct 1);
 by (Auto_tac());
 by (etac analz.induct 1);
-by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
+by (ALLGOALS
+    (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
 qed "analz_insert_MPair";
 
 (*Can pull out enCrypted message if the Key is not known*)
@@ -412,12 +413,12 @@
 (*Case analysis: either the message is secure, or it is not!
   Effective, but can cause subgoals to blow up!
   Use with expand_if;  apparently split_tac does not cope with patterns
-  such as "analz (insert (Crypt X' K) H)" *)
-goal thy "analz (insert (Crypt X' K) H) = \
+  such as "analz (insert (Crypt X K) H)" *)
+goal thy "analz (insert (Crypt X K) H) = \
 \         (if (Key (invKey K)  : analz H) then    \
-\               insert (Crypt X' K) (analz (insert X' H)) \
-\          else insert (Crypt X' K) (analz H))";
-by (excluded_middle_tac "Key (invKey K)  : analz H " 1);
+\               insert (Crypt X K) (analz (insert X H)) \
+\          else insert (Crypt X K) (analz H))";
+by (case_tac "Key (invKey K)  : analz H " 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
                                                analz_insert_Decrypt])));
 qed "analz_Crypt_if";
diff -r 5d44339454a4 -r 41a667d2c3fa src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Fri Oct 18 11:32:38 1996 +0200
+++ b/src/HOL/ex/Primes.ML	Fri Oct 18 11:33:02 1996 +0200
@@ -92,9 +92,9 @@
 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);
@@ -126,9 +126,9 @@
 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);