src/HOL/Auth/OtwayRees.ML
changeset 2171 91b4161a28e5
parent 2166 d276a806cc10
child 2194 63a68a3a8a76
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Nov 08 14:13:56 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Nov 08 16:32:57 1996 +0100
     1.3 @@ -93,9 +93,9 @@
     1.4  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
     1.5  fun parts_induct_tac i = SELECT_GOAL
     1.6      (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
     1.7 -	     (*Fake message*)
     1.8 -	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     1.9 -					   impOfSubs Fake_parts_insert]
    1.10 +             (*Fake message*)
    1.11 +             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.12 +                                           impOfSubs Fake_parts_insert]
    1.13                                      addss (!simpset)) 2)) THEN
    1.14       (*Base case*)
    1.15       fast_tac (!claset addss (!simpset)) 1 THEN
    1.16 @@ -460,7 +460,7 @@
    1.17  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    1.18  (*Oops*) (** LEVEL 5 **)
    1.19  by (fast_tac (!claset delrules [disjE]
    1.20 -		      addDs [unique_session_keys] addss (!simpset)) 1);
    1.21 +                      addDs [unique_session_keys] addss (!simpset)) 1);
    1.22  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.23  
    1.24  goal thy 
    1.25 @@ -559,7 +559,7 @@
    1.26  (*OR3 and OR4*)  (** LEVEL 5 **)
    1.27  (*OR4*)
    1.28  by (REPEAT (Safe_step_tac 2));
    1.29 -br (Crypt_imp_OR2 RS exE) 2;
    1.30 +by (rtac (Crypt_imp_OR2 RS exE) 2);
    1.31  by (REPEAT (fast_tac (!claset addEs partsEs) 2));
    1.32  (*OR3*)  (** LEVEL 8 **)
    1.33  by (step_tac (!claset delrules [disjCI, impCE]) 1);