Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Attic/Unused.thy
changeset 980 9d35c6145dd2
parent 948 25c4223635f4
child 1024 b3deb964ad26 
--- a/Attic/Unused.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Attic/Unused.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -6,9 +6,9 @@
   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)
+  "Bex1_rel" :: "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)"
+  "\<exists>!!x\<in>A. P"  == "Bex1_rel A (%x. P)"
 
 
 (* Atomize infrastructure *)
nominal2