src/HOL/Auth/Shared.ML
changeset 4238 679a233fb206
parent 4156 31251763848d
child 4369 11b217d9d880
     1.1 --- a/src/HOL/Auth/Shared.ML	Tue Nov 18 16:36:33 1997 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Tue Nov 18 16:37:25 1997 +0100
     1.3 @@ -28,6 +28,11 @@
     1.4  qed "keysFor_parts_initState";
     1.5  Addsimps [keysFor_parts_initState];
     1.6  
     1.7 +goal thy "!!H. Crypt K X : H ==> K : keysFor H";
     1.8 +by (dtac Crypt_imp_invKey_keysFor 1);
     1.9 +by (Asm_full_simp_tac 1);
    1.10 +qed "Crypt_imp_keysFor";
    1.11 +
    1.12  
    1.13  (*** Function "spies" ***)
    1.14