# HG changeset patch
# User paulson
# Date 875183534 -7200
# Node ID ab3b4ceb61dc037c71cd74fabbc833705dd4e03f
# Parent  8a1f7d5b1eff9e4d0b08603d634d98365313072e
Deleted obsolete version of clarify_tac

diff -r 8a1f7d5b1eff -r ab3b4ceb61dc src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Sep 25 12:25:29 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Sep 25 12:32:14 1997 +0200
@@ -13,19 +13,6 @@
 by (Blast_tac 1);
 Addsimps [result()];
 
-
-(*Classical simplification*)
-val rev_conjI = conjI RS (conj_commute RS iffD1) |> standard;
-val acontr_tac = assume_tac ORELSE' contr_tac;
-fun impCE_tac i = eresolve_tac [impCE] i  THEN  
-                (acontr_tac i ORELSE acontr_tac (i+1));
-
-val clarify_tac =
-    REPEAT_FIRST (ares_tac [impI, notI, allI] ORELSE'
-		  eresolve_tac [exE, conjE, conjI, rev_conjI] ORELSE'
-		  contr_tac ORELSE' impCE_tac ORELSE' hyp_subst_tac);
-
-
 open Message;
 
 AddIffs atomic.inject;
@@ -547,7 +534,7 @@
 
 goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
 \              |] ==> analz (G Un H) <= analz (G' Un H')";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (etac analz.induct 1);
 by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD])));
 qed "analz_subset_cong";