# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260526373 -3600
# Node ID 6decb8811d30b6b211f6b5e67bf12d74fd2cd7cf
# Parent  84e2e4649b48fe32e88d2d803c8f96ac41469d2d
tuned

diff -r 84e2e4649b48 -r 6decb8811d30 Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Fri Dec 11 10:57:46 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Fri Dec 11 11:12:53 2009 +0100
@@ -165,7 +165,7 @@
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
 quotient_def
-  nonces :: "nounces:: msg \<Rightarrow> nat set"
+  nonces :: "nonces:: msg \<Rightarrow> nat set"
 where
   "freenonces"