Now the possibility proof calls the appropriate tactic
authorpaulson
Tue Jul 01 10:38:11 1997 +0200 (1997-07-01)
changeset 3471cd37ec057028
parent 3470 8160cc3f6d40
child 3472 fb3c38c88c08
Now the possibility proof calls the appropriate tactic
src/HOL/Auth/WooLam.ML
     1.1 --- a/src/HOL/Auth/WooLam.ML	Tue Jul 01 10:37:42 1997 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.ML	Tue Jul 01 10:38:11 1997 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 -Pretty.setdepth 20;
     1.8  
     1.9  
    1.10  (*A "possibility property": there are traces that reach the end*)
    1.11 @@ -25,9 +24,7 @@
    1.12  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.13  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
    1.14            woolam.WL4 RS woolam.WL5) 2);
    1.15 -by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
    1.16 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.17 -by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE])));
    1.18 +by possibility_tac;
    1.19  result();
    1.20  
    1.21  
    1.22 @@ -56,7 +53,7 @@
    1.23  val parts_induct_tac = 
    1.24      etac woolam.induct 1  THEN 
    1.25      forward_tac [WL4_parts_sees_Spy] 6  THEN
    1.26 -    prove_simple_subgoals_tac  1;
    1.27 +    prove_simple_subgoals_tac 1;
    1.28  
    1.29  
    1.30  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY