# HG changeset patch
# User paulson
# Date 845631737 -7200
# Node ID fabc35243ceab2ebddafbe677059b6f89d768fe9
# Parent  17fca2a71f8d7c85212aef404da330517e6d8eeb
Deleted obsolete rewrites (they are now in HOL/simpdata)

diff -r 17fca2a71f8d -r fabc35243cea src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Oct 18 11:41:41 1996 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Oct 18 11:42:17 1996 +0200
@@ -9,14 +9,9 @@
 *)
 
 
-Addsimps [de_Morgan_conj, de_Morgan_disj, not_all, not_ex];
-(**Addsimps [all_conj_distrib, ex_disj_distrib];**)
-
-
 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
-by (excluded_middle_tac "P" 1);
-by (asm_simp_tac (!simpset addsimps prems) 1);
-by (asm_simp_tac (!simpset addsimps prems) 1);
+by (case_tac "P" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
 val expand_case = result();
 
 fun expand_case_tac P i =