# HG changeset patch
# User paulson
# Date 875096681 -7200
# Node ID 6f0ed3eef1a9c43ccf35e4b7e4a616dc6b323dc9
# Parent  3a8192e83579109138015c19a2e4c6ddb5e4514f
Names and saves the theorem parts_spies_subset_used

diff -r 3a8192e83579 -r 6f0ed3eef1a9 src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Wed Sep 24 10:51:52 1997 +0200
+++ b/src/HOL/Auth/Event.ML	Wed Sep 24 12:24:41 1997 +0200
@@ -82,7 +82,9 @@
 	      (!simpset addsimps [parts_insert_spies]
 	                setloop split_tac [expand_event_case, expand_if])));
 by (ALLGOALS Blast_tac);
-bind_thm ("usedI", impOfSubs (result()));
+qed "parts_spies_subset_used";
+
+bind_thm ("usedI", impOfSubs parts_spies_subset_used);
 AddIs [usedI];
 
 goal thy "parts (initState B) <= used evs";