# HG changeset patch
# User paulson
# Date 867746291 -7200
# Node ID cd37ec057028d5bc15015360b65df8d4a3623393
# Parent  8160cc3f6d4003400f505a97c51e8d4896a83199
Now the possibility proof calls the appropriate tactic

diff -r 8160cc3f6d40 -r cd37ec057028 src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Tue Jul 01 10:37:42 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML	Tue Jul 01 10:38:11 1997 +0200
@@ -14,7 +14,6 @@
 
 proof_timing:=true;
 HOL_quantifiers := false;
-Pretty.setdepth 20;
 
 
 (*A "possibility property": there are traces that reach the end*)
@@ -25,9 +24,7 @@
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
           woolam.WL4 RS woolam.WL5) 2);
-by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
-by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE])));
+by possibility_tac;
 result();
 
 
@@ -56,7 +53,7 @@
 val parts_induct_tac = 
     etac woolam.induct 1  THEN 
     forward_tac [WL4_parts_sees_Spy] 6  THEN
-    prove_simple_subgoals_tac  1;
+    prove_simple_subgoals_tac 1;
 
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY