Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed quot_respect attribute of a non-standard lemma
authorChristian Urban <urbanc@in.tum.de>
Thu, 10 Dec 2009 02:46:08 +0100
changeset 680 d003f9e00c29
parent 678 569f0e286400
child 681 3c6419a5a7fc
removed quot_respect attribute of a non-standard lemma
Quot/Examples/FSet.thy file | annotate | diff | comparison | revisions 
--- 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