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/FSet.thy
changeset 680 d003f9e00c29
parent 664 546ba31fbb83
child 681 3c6419a5a7fc 
--- a/Quot/Examples/FSet.thy	Thu Dec 10 01:48:39 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 02:46:08 2009 +0100
@@ -151,7 +151,7 @@
   "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
nominal2