small simplification to not_Says_to_self
authorpaulson
Wed Sep 02 10:35:11 1998 +0200 (1998-09-02)
changeset 542101fc8d6a40f2
parent 5420 b48ab3281944
child 5422 578dc167453f
small simplification to not_Says_to_self
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 01 15:07:11 1998 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Sep 02 10:35:11 1998 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  (**** Inductive proofs about kerberos_ban ****)
     1.5  
     1.6  (*Nobody sends themselves messages*)
     1.7 -Goal "evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
     1.8 +Goal "evs : kerberos_ban ==> ALL X. Says A A X ~: set evs";
     1.9  by (etac kerberos_ban.induct 1);
    1.10  by Auto_tac;
    1.11  qed_spec_mp "not_Says_to_self";
     2.1 --- a/src/HOL/Auth/Message.ML	Tue Sep 01 15:07:11 1998 +0200
     2.2 +++ b/src/HOL/Auth/Message.ML	Wed Sep 02 10:35:11 1998 +0200
     2.3 @@ -862,8 +862,7 @@
     2.4    concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
     2.5    alone.*)
     2.6  fun prove_simple_subgoals_tac i = 
     2.7 -    fast_tac (claset() addss (simpset())) i THEN
     2.8 -    ALLGOALS Asm_simp_tac;
     2.9 +    Force_tac i THEN ALLGOALS Asm_simp_tac;
    2.10  
    2.11  fun Fake_parts_insert_tac i = 
    2.12      blast_tac (claset() addIs [parts_insertI]
     3.1 --- a/src/HOL/Auth/NS_Public.ML	Tue Sep 01 15:07:11 1998 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public.ML	Wed Sep 02 10:35:11 1998 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4  (**** Inductive proofs about ns_public ****)
     3.5  
     3.6  (*Nobody sends themselves messages*)
     3.7 -Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs";
     3.8 +Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
     3.9  by (etac ns_public.induct 1);
    3.10  by Auto_tac;
    3.11  qed_spec_mp "not_Says_to_self";
     4.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 01 15:07:11 1998 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Sep 02 10:35:11 1998 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4  (**** Inductive proofs about ns_public ****)
     4.5  
     4.6  (*Nobody sends themselves messages*)
     4.7 -Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs";
     4.8 +Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
     4.9  by (etac ns_public.induct 1);
    4.10  by Auto_tac;
    4.11  qed_spec_mp "not_Says_to_self";
     5.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 01 15:07:11 1998 +0200
     5.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Sep 02 10:35:11 1998 +0200
     5.3 @@ -36,7 +36,7 @@
     5.4  (**** Inductive proofs about ns_shared ****)
     5.5  
     5.6  (*Nobody sends themselves messages*)
     5.7 -Goal "evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
     5.8 +Goal "evs : ns_shared ==> ALL X. Says A A X ~: set evs";
     5.9  by (etac ns_shared.induct 1);
    5.10  by Auto_tac;
    5.11  qed_spec_mp "not_Says_to_self";
     6.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 01 15:07:11 1998 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed Sep 02 10:35:11 1998 +0200
     6.3 @@ -31,7 +31,7 @@
     6.4  (**** Inductive proofs about otway ****)
     6.5  
     6.6  (*Nobody sends themselves messages*)
     6.7 -Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
     6.8 +Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
     6.9  by (etac otway.induct 1);
    6.10  by Auto_tac;
    6.11  qed_spec_mp "not_Says_to_self";
     7.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 01 15:07:11 1998 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 02 10:35:11 1998 +0200
     7.3 @@ -31,7 +31,7 @@
     7.4  (**** Inductive proofs about otway ****)
     7.5  
     7.6  (*Nobody sends themselves messages*)
     7.7 -Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
     7.8 +Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
     7.9  by (etac otway.induct 1);
    7.10  by Auto_tac;
    7.11  qed_spec_mp "not_Says_to_self";
     8.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 01 15:07:11 1998 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Sep 02 10:35:11 1998 +0200
     8.3 @@ -34,7 +34,7 @@
     8.4  (**** Inductive proofs about otway ****)
     8.5  
     8.6  (*Nobody sends themselves messages*)
     8.7 -Goal "evs : otway ==> ALL A X. Says A A X ~: set evs";
     8.8 +Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
     8.9  by (etac otway.induct 1);
    8.10  by Auto_tac;
    8.11  qed_spec_mp "not_Says_to_self";
     9.1 --- a/src/HOL/Auth/Recur.ML	Tue Sep 01 15:07:11 1998 +0200
     9.2 +++ b/src/HOL/Auth/Recur.ML	Wed Sep 02 10:35:11 1998 +0200
     9.3 @@ -71,7 +71,7 @@
     9.4  (**** Inductive proofs about recur ****)
     9.5  
     9.6  (*Nobody sends themselves messages*)
     9.7 -Goal "evs : recur ==> ALL A X. Says A A X ~: set evs";
     9.8 +Goal "evs : recur ==> ALL X. Says A A X ~: set evs";
     9.9  by (etac recur.induct 1);
    9.10  by Auto_tac;
    9.11  qed_spec_mp "not_Says_to_self";
    10.1 --- a/src/HOL/Auth/TLS.ML	Tue Sep 01 15:07:11 1998 +0200
    10.2 +++ b/src/HOL/Auth/TLS.ML	Wed Sep 02 10:35:11 1998 +0200
    10.3 @@ -119,7 +119,7 @@
    10.4  (**** Inductive proofs about tls ****)
    10.5  
    10.6  (*Nobody sends themselves messages*)
    10.7 -Goal "evs : tls ==> ALL A X. Says A A X ~: set evs";
    10.8 +Goal "evs : tls ==> ALL X. Says A A X ~: set evs";
    10.9  by (etac tls.induct 1);
   10.10  by Auto_tac;
   10.11  qed_spec_mp "not_Says_to_self";
    11.1 --- a/src/HOL/Auth/WooLam.ML	Tue Sep 01 15:07:11 1998 +0200
    11.2 +++ b/src/HOL/Auth/WooLam.ML	Wed Sep 02 10:35:11 1998 +0200
    11.3 @@ -29,7 +29,7 @@
    11.4  (**** Inductive proofs about woolam ****)
    11.5  
    11.6  (*Nobody sends themselves messages*)
    11.7 -Goal "evs : woolam ==> ALL A X. Says A A X ~: set evs";
    11.8 +Goal "evs : woolam ==> ALL X. Says A A X ~: set evs";
    11.9  by (etac woolam.induct 1);
   11.10  by Auto_tac;
   11.11  qed_spec_mp "not_Says_to_self";
    12.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Sep 01 15:07:11 1998 +0200
    12.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 02 10:35:11 1998 +0200
    12.3 @@ -27,7 +27,7 @@
    12.4  (**** Inductive proofs about yahalom ****)
    12.5  
    12.6  (*Nobody sends themselves messages*)
    12.7 -Goal "evs: yahalom ==> ALL A X. Says A A X ~: set evs";
    12.8 +Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
    12.9  by (etac yahalom.induct 1);
   12.10  by Auto_tac;
   12.11  qed_spec_mp "not_Says_to_self";
    13.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 01 15:07:11 1998 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Sep 02 10:35:11 1998 +0200
    13.3 @@ -31,7 +31,7 @@
    13.4  (**** Inductive proofs about yahalom ****)
    13.5  
    13.6  (*Nobody sends themselves messages*)
    13.7 -Goal "evs: yahalom ==> ALL A X. Says A A X ~: set evs";
    13.8 +Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
    13.9  by (etac yahalom.induct 1);
   13.10  by Auto_tac;
   13.11  qed_spec_mp "not_Says_to_self";