# HG changeset patch
# User paulson
# Date 904725311 -7200
# Node ID 01fc8d6a40f2ae424595ee4cadd3149a5495acb7
# Parent  b48ab3281944d2f780fec6e092c599d2787add46
small simplification to not_Says_to_self

diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -42,7 +42,7 @@
 (**** Inductive proofs about kerberos_ban ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : kerberos_ban ==> ALL X. Says A A X ~: set evs";
 by (etac kerberos_ban.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/Message.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -862,8 +862,7 @@
   concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    fast_tac (claset() addss (simpset())) i THEN
-    ALLGOALS Asm_simp_tac;
+    Force_tac i THEN ALLGOALS Asm_simp_tac;
 
 fun Fake_parts_insert_tac i = 
     blast_tac (claset() addIs [parts_insertI]
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -25,7 +25,7 @@
 (**** Inductive proofs about ns_public ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
 by (etac ns_public.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -29,7 +29,7 @@
 (**** Inductive proofs about ns_public ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
 by (etac ns_public.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -36,7 +36,7 @@
 (**** Inductive proofs about ns_shared ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : ns_shared ==> ALL X. Says A A X ~: set evs";
 by (etac ns_shared.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -31,7 +31,7 @@
 (**** Inductive proofs about otway ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
 by (etac otway.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -31,7 +31,7 @@
 (**** Inductive proofs about otway ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
 by (etac otway.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -34,7 +34,7 @@
 (**** Inductive proofs about otway ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
 by (etac otway.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/Recur.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -71,7 +71,7 @@
 (**** Inductive proofs about recur ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : recur ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : recur ==> ALL X. Says A A X ~: set evs";
 by (etac recur.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/TLS.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -119,7 +119,7 @@
 (**** Inductive proofs about tls ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : tls ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : tls ==> ALL X. Says A A X ~: set evs";
 by (etac tls.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/WooLam.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -29,7 +29,7 @@
 (**** Inductive proofs about woolam ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs : woolam ==> ALL A X. Says A A X ~: set evs";
+Goal "evs : woolam ==> ALL X. Says A A X ~: set evs";
 by (etac woolam.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -27,7 +27,7 @@
 (**** Inductive proofs about yahalom ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL A X. Says A A X ~: set evs";
+Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
 by (etac yahalom.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";
diff -r b48ab3281944 -r 01fc8d6a40f2 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 01 15:07:11 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Wed Sep 02 10:35:11 1998 +0200
@@ -31,7 +31,7 @@
 (**** Inductive proofs about yahalom ****)
 
 (*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL A X. Says A A X ~: set evs";
+Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
 by (etac yahalom.induct 1);
 by Auto_tac;
 qed_spec_mp "not_Says_to_self";