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