# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260555590 -3600
# Node ID 93dce7c719290b280835101139db998b872300ea
# Parent  d5fce1ead4322267e1a8fbd520357fbb74461827
tuned

diff -r d5fce1ead432 -r 93dce7c71929 Quot/Examples/LarryDatatype.thy
--- 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