--- a/src/HOL/Auth/Guard/Extensions.thy Fri Dec 19 17:13:28 2003 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Sun Dec 21 08:27:44 2003 +0100
@@ -13,6 +13,7 @@
theory Extensions = Event:
+declare insert_Diff_single [simp del]
subsection{*Extensions to Theory @{text Set}*}