Reformatting
authorpaulson
Fri Sep 13 18:47:01 1996 +0200 (1996-09-13)
changeset 1999b5efc4108d04
parent 1998 f8230821f1e8
child 2000 adb88d42f1bd
Reformatting
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 18:46:08 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 18:47:01 1996 +0200
     1.3 @@ -68,8 +68,8 @@
     1.4  
     1.5  (*Enemy never sees another agent's shared key!*)
     1.6  goal thy 
     1.7 - "!!evs. [| evs : ns_shared; A ~: bad |] ==> \
     1.8 -\        Key (shrK A) ~: parts (sees Enemy evs)";
     1.9 + "!!evs. [| evs : ns_shared; A ~: bad |]    \
    1.10 +\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    1.11  be ns_shared.induct 1;
    1.12  bd NS3_msg_in_parts_sees_Enemy 5;
    1.13  by (Auto_tac());
    1.14 @@ -136,8 +136,8 @@
    1.15  
    1.16  (*Variant needed for the main theorem below*)
    1.17  goal thy 
    1.18 - "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
    1.19 -\        Key (newK evs') ~: parts (sees C evs)";
    1.20 + "!!evs. [| evs : ns_shared;  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 @@ -179,8 +179,8 @@
    1.26  val lemma = result();
    1.27  
    1.28  goal thy 
    1.29 - "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
    1.30 -\        newK evs' ~: keysFor (parts (sees C evs))";
    1.31 + "!!evs. [| evs : ns_shared;  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  
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 18:46:08 1996 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 18:47:01 1996 +0200
     2.3 @@ -91,8 +91,8 @@
     2.4  
     2.5  (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
     2.6  goal thy 
     2.7 - "!!evs. [| evs : otway;  A ~: bad |] ==> \
     2.8 -\        Key (shrK A) ~: parts (sees Enemy evs)";
     2.9 + "!!evs. [| evs : otway;  A ~: bad |]    \
    2.10 +\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    2.11  be otway.induct 1;
    2.12  by OR2_OR4_tac;
    2.13  by (Auto_tac());
    2.14 @@ -148,8 +148,8 @@
    2.15  
    2.16  (*Variant needed for the main theorem below*)
    2.17  goal thy 
    2.18 - "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
    2.19 -\        Key (newK evs') ~: parts (sees C evs)";
    2.20 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
    2.21 +\        ==> Key (newK evs') ~: parts (sees C evs)";
    2.22  by (fast_tac (!claset addDs [lemma]) 1);
    2.23  qed "new_keys_not_seen";
    2.24  Addsimps [new_keys_not_seen];
    2.25 @@ -194,8 +194,8 @@
    2.26  val lemma = result();
    2.27  
    2.28  goal thy 
    2.29 - "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
    2.30 -\        newK evs' ~: keysFor (parts (sees C evs))";
    2.31 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
    2.32 +\        ==> newK evs' ~: keysFor (parts (sees C evs))";
    2.33  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    2.34  qed "new_keys_not_used";
    2.35