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 515 b00a9b58264d
parent 511 28bb34eeedc5
child 516 bed81795848c 
--- a/QuotScript.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -137,7 +137,7 @@
 
 lemma FUN_REL_EQ:
   "(op =) ===> (op =) \<equiv> (op =)"
-by (simp add: expand_fun_eq)
+by (rule eq_reflection) (simp add: expand_fun_eq)
 
 lemma FUN_QUOTIENT:
   assumes q1: "QUOTIENT R1 abs1 rep1"
nominal2