src/HOL/Auth/OtwayRees.ML
changeset 1999 b5efc4108d04
parent 1996 33c42cae3dd0
child 2014 5be4c8ca7b25
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 18:46:08 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 18:47:01 1996 +0200
     1.3 @@ -91,8 +91,8 @@
     1.4  
     1.5  (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
     1.6  goal thy 
     1.7 - "!!evs. [| evs : otway;  A ~: bad |] ==> \
     1.8 -\        Key (shrK A) ~: parts (sees Enemy evs)";
     1.9 + "!!evs. [| evs : otway;  A ~: bad |]    \
    1.10 +\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    1.11  be otway.induct 1;
    1.12  by OR2_OR4_tac;
    1.13  by (Auto_tac());
    1.14 @@ -148,8 +148,8 @@
    1.15  
    1.16  (*Variant needed for the main theorem below*)
    1.17  goal thy 
    1.18 - "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
    1.19 -\        Key (newK evs') ~: parts (sees C evs)";
    1.20 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
    1.21 +\        ==> Key (newK evs') ~: parts (sees C evs)";
    1.22  by (fast_tac (!claset addDs [lemma]) 1);
    1.23  qed "new_keys_not_seen";
    1.24  Addsimps [new_keys_not_seen];
    1.25 @@ -194,8 +194,8 @@
    1.26  val lemma = result();
    1.27  
    1.28  goal thy 
    1.29 - "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
    1.30 -\        newK evs' ~: keysFor (parts (sees C evs))";
    1.31 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
    1.32 +\        ==> newK evs' ~: keysFor (parts (sees C evs))";
    1.33  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    1.34  qed "new_keys_not_used";
    1.35