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.
Quot/QuotProd.thy
changeset 925 8d51795ef54d
parent 922 a2589b4bc442
child 928 44c92eaa4fad
child 935 c96e007b512f 
--- a/Quot/QuotProd.thy	Mon Jan 25 20:35:42 2010 +0100
+++ b/Quot/QuotProd.thy	Mon Jan 25 20:47:20 2010 +0100
@@ -80,7 +80,7 @@
      (simp add: prod_fun_def)
 
 lemma prod_rel_eq[id_simps]: 
-  shows "prod_rel op = op = \<equiv> op ="
+  shows "prod_rel (op =) (op =) \<equiv> (op =)"
   apply (rule eq_reflection)
   apply (rule ext)+
   apply auto
nominal2