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.
UnusedQuotMain.thy
changeset 401 211229d6c66f
parent 399 646bfe5905b3
child 466 42082fc00903 
--- a/UnusedQuotMain.thy	Thu Nov 26 20:32:33 2009 +0100
+++ b/UnusedQuotMain.thy	Thu Nov 26 20:32:56 2009 +0100
@@ -484,7 +484,7 @@
 
 
 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
-ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *}
+ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}
nominal2