# HG changeset patch
# User paulson
# Date 877944857 -3600
# Node ID 84a5efc95dcfe0be99e5a7ce84f7278d38aa447a
# Parent  8858c472691a6d357a84683cbeabb7d2fe60aa1c
Deleted two needless theorems

diff -r 8858c472691a -r 84a5efc95dcf src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Sat Oct 25 14:43:55 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Mon Oct 27 10:34:17 1997 +0100
@@ -19,12 +19,6 @@
 
 open TLS;
 
-val if_distrib_parts = 
-    read_instantiate_sg (sign_of Message.thy) [("f", "parts")] if_distrib;
-
-val if_distrib_analz = 
-    read_instantiate_sg (sign_of Message.thy) [("f", "analz")] if_distrib;
-
 proof_timing:=true;
 HOL_quantifiers := false;