--- 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";