# HG changeset patch
# User nipkow
# Date 1071991664 -3600
# Node ID 1d40d90398eb89bbf82bf0654748b8574a803c8b
# Parent  f17ca9f6dc8c28a8fd359c8f12e210b128545fea
removed insert_Diff_single from simpset because it interfered with Auth :-(

diff -r f17ca9f6dc8c -r 1d40d90398eb src/HOL/Auth/Guard/Extensions.thy
--- 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}*}