# HG changeset patch
# User paulson
# Date 1128066766 -7200
# Node ID d74d0b5052a01ce764995d4c802640839c8a9034
# Parent  1412f84c420aec5b526e994e690c973352aa75b3
theorems need names

diff -r 1412f84c420a -r d74d0b5052a0 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Sep 29 19:37:20 2005 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Sep 30 09:52:46 2005 +0200
@@ -226,7 +226,8 @@
 
 text{*This allows @{text blast} to simplify occurrences of 
   @{term "parts(G\<union>H)"} in the assumption.*}
-declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!] 
+lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
+declare in_parts_UnE [elim!]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"