# HG changeset patch
# User paulson
# Date 842633221 -7200
# Node ID b5efc4108d045016d012c3dae980b70d8f0af6fe
# Parent  f8230821f1e84e23dff57064ccc91dc0561422f4
Reformatting

diff -r f8230821f1e8 -r b5efc4108d04 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 18:46:08 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Sep 13 18:47:01 1996 +0200
@@ -68,8 +68,8 @@
 
 (*Enemy never sees another agent's shared key!*)
 goal thy 
- "!!evs. [| evs : ns_shared; A ~: bad |] ==> \
-\        Key (shrK A) ~: parts (sees Enemy evs)";
+ "!!evs. [| evs : ns_shared; A ~: bad |]    \
+\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
 be ns_shared.induct 1;
 bd NS3_msg_in_parts_sees_Enemy 5;
 by (Auto_tac());
@@ -136,8 +136,8 @@
 
 (*Variant needed for the main theorem below*)
 goal thy 
- "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
-\        Key (newK evs') ~: parts (sees C evs)";
+ "!!evs. [| evs : ns_shared;  length evs <= length evs' |]    \
+\        ==> Key (newK evs') ~: parts (sees C evs)";
 by (fast_tac (!claset addDs [lemma]) 1);
 qed "new_keys_not_seen";
 Addsimps [new_keys_not_seen];
@@ -179,8 +179,8 @@
 val lemma = result();
 
 goal thy 
- "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
-\        newK evs' ~: keysFor (parts (sees C evs))";
+ "!!evs. [| evs : ns_shared;  length evs <= length evs' |]    \
+\        ==> newK evs' ~: keysFor (parts (sees C evs))";
 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
 qed "new_keys_not_used";
 
diff -r f8230821f1e8 -r b5efc4108d04 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 18:46:08 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 18:47:01 1996 +0200
@@ -91,8 +91,8 @@
 
 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
 goal thy 
- "!!evs. [| evs : otway;  A ~: bad |] ==> \
-\        Key (shrK A) ~: parts (sees Enemy evs)";
+ "!!evs. [| evs : otway;  A ~: bad |]    \
+\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
 be otway.induct 1;
 by OR2_OR4_tac;
 by (Auto_tac());
@@ -148,8 +148,8 @@
 
 (*Variant needed for the main theorem below*)
 goal thy 
- "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
-\        Key (newK evs') ~: parts (sees C evs)";
+ "!!evs. [| evs : otway;  length evs <= length evs' |]    \
+\        ==> Key (newK evs') ~: parts (sees C evs)";
 by (fast_tac (!claset addDs [lemma]) 1);
 qed "new_keys_not_seen";
 Addsimps [new_keys_not_seen];
@@ -194,8 +194,8 @@
 val lemma = result();
 
 goal thy 
- "!!evs. [| evs : otway;  length evs <= length evs' |] ==> \
-\        newK evs' ~: keysFor (parts (sees C evs))";
+ "!!evs. [| evs : otway;  length evs <= length evs' |]    \
+\        ==> newK evs' ~: keysFor (parts (sees C evs))";
 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
 qed "new_keys_not_used";