diff -r 95ee248b3832 -r aa960d16570f Unused.thy
--- a/Unused.thy	Thu Jan 21 12:03:47 2010 +0100
+++ b/Unused.thy	Thu Jan 21 12:50:43 2010 +0100
@@ -5,6 +5,10 @@
   shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
   by(auto simp add: QUOT_TRUE_def)
 
+syntax
+  "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
+translations
+  "\<exists>!!x\<in>A. P"  == "Bexeq A (%x. P)"
 
 
 (* Atomize infrastructure *)