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.
abs_rep as ==
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 04 Dec 2009 18:32:19 +0100 (2009-12-04)
changeset 546 8a1f4227dff9
parent 545 95371a8b17e1
child 547 b0809b256a88
child 549 f178958d3d81
abs_rep as ==
QuotScript.thy file | annotate | diff | comparison | revisions 
--- a/QuotScript.thy	Fri Dec 04 17:57:03 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 18:32:19 2009 +0100
@@ -43,7 +43,7 @@
 
 lemma Quotient_abs_rep:
   assumes a: "Quotient E Abs Rep"
-  shows "Abs (Rep a) = a"
+  shows "Abs (Rep a) \<equiv> a"
   using a unfolding Quotient_def
   by simp
nominal2