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.
QuotScript.thy
changeset 511 28bb34eeedc5
parent 459 020e27417b59
child 515 b00a9b58264d 
--- a/QuotScript.thy	Fri Dec 04 09:10:31 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:18:46 2009 +0100
@@ -136,7 +136,7 @@
   "E1 ===> E2 \<equiv> FUN_REL E1 E2"
 
 lemma FUN_REL_EQ:
-  "(op =) ===> (op =) = (op =)"
+  "(op =) ===> (op =) \<equiv> (op =)"
 by (simp add: expand_fun_eq)
 
 lemma FUN_QUOTIENT:
nominal2