# HG changeset patch
# User paulson
# Date 850730891 -3600
# Node ID 95f275c8476e58fe5fd95344da145c342ed2d37d
# Parent  8ba800a46e14372cba02ebce903bc0352e7b2966
New tactic: prove_unique_tac

diff -r 8ba800a46e14 -r 95f275c8476e src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Mon Dec 16 10:50:08 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Mon Dec 16 11:08:11 1996 +0100
@@ -306,11 +306,7 @@
 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
 \            : set_of_list evs;                                    \
 \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
 
 
@@ -349,12 +345,7 @@
 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
 \          evs : otway lost;  A ~: lost |]                                    \
 \        ==> B = C";
-by (dtac lemma 1);
-by (assume_tac 1);
-by (etac exE 1);
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_NA";
 
 
@@ -529,12 +520,7 @@
 \                  : parts(sees lost Spy evs);         \
 \          evs : otway lost;  B ~: lost |]             \
 \        ==> NC = NA & C = A";
-by (dtac lemma 1);
-by (assume_tac 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_NB";
 
 
diff -r 8ba800a46e14 -r 95f275c8476e src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Dec 16 10:50:08 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Dec 16 11:08:11 1996 +0100
@@ -276,11 +276,7 @@
 \           : set_of_list evs;                                     \
 \          evs : otway lost |]                                     \
 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
 
 
diff -r 8ba800a46e14 -r 95f275c8476e src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Dec 16 10:50:08 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Dec 16 11:08:11 1996 +0100
@@ -317,11 +317,7 @@
 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
 \            : set_of_list evs;                                    \
 \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
 qed "unique_session_keys";