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/Examples/LarryInt.thy
changeset 913 b1f55dd64481
parent 804 ba7e81531c6d
child 1128 17ca92ab4660 
--- a/Quot/Examples/LarryInt.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -178,7 +178,7 @@
 
 lemma [quot_respect]:
   shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel.simps)
+apply(simp only: fun_rel_def)
 apply(rule allI | rule impI)+
 apply(rule equivp_transp[OF int_equivp])
 apply(rule mult_raw_fst)
nominal2