Deleted two needless theorems
authorpaulson
Mon Oct 27 10:34:17 1997 +0100 (1997-10-27)
changeset 400684a5efc95dcf
parent 4005 8858c472691a
child 4007 1d6aed7ff375
Deleted two needless theorems
src/HOL/Auth/TLS.ML
     1.1 --- a/src/HOL/Auth/TLS.ML	Sat Oct 25 14:43:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Mon Oct 27 10:34:17 1997 +0100
     1.3 @@ -19,12 +19,6 @@
     1.4  
     1.5  open TLS;
     1.6  
     1.7 -val if_distrib_parts = 
     1.8 -    read_instantiate_sg (sign_of Message.thy) [("f", "parts")] if_distrib;
     1.9 -
    1.10 -val if_distrib_analz = 
    1.11 -    read_instantiate_sg (sign_of Message.thy) [("f", "analz")] if_distrib;
    1.12 -
    1.13  proof_timing:=true;
    1.14  HOL_quantifiers := false;
    1.15