Mercurial Mercurial > repos > isabelle / 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.
unsymbolize;
authorwenzelm
Tue, 21 Nov 2000 19:03:06 +0100
changeset 10505 b89e6cc963e3
parent 10504 d7f5607fbadf
child 10506 01333dbe1431
unsymbolize;
src/HOL/Library/Quotient.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Quotient.thy	Tue Nov 21 19:02:31 2000 +0100
+++ b/src/HOL/Library/Quotient.thy	Tue Nov 21 19:03:06 2000 +0100
@@ -185,7 +185,7 @@
   assume cong: "PROP ?cong"
   assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
-  also have "\<dots> = g a b"
+  also have "... = g a b"
   proof (rule cong)
     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
     moreover
isabelle