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 113 e3a963e6418b
parent 112 0d6d37d0589d
child 126 9cb8f9a59402 
--- a/QuotScript.thy	Fri Oct 16 16:51:01 2009 +0200
+++ b/QuotScript.thy	Fri Oct 16 17:05:52 2009 +0200
@@ -307,8 +307,14 @@
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using a
-by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+  and   "R (Rep (Abs x1)) x2"
+proof -
+  show "R x1 (Rep (Abs x2))" 
+    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+next
+  show "R (Rep (Abs x1)) x2"
+    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
+qed
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
nominal2