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.
tuned
authorChristian Urban <urbanc@in.tum.de>
Fri, 11 Dec 2009 19:19:50 +0100
changeset 723 93dce7c71929
parent 722 d5fce1ead432
child 724 d705d7ae2410
tuned
Quot/Examples/LarryDatatype.thy file | annotate | diff | comparison | revisions 
--- a/Quot/Examples/LarryDatatype.thy	Fri Dec 11 19:19:24 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Fri Dec 11 19:19:50 2009 +0100
@@ -119,7 +119,6 @@
   shows "freediscrim U = freediscrim V"
 using a by (induct, auto)
 
-
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
 quotient  msg = freemsg / msgrel
nominal2