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 11:12:53 +0100
changeset 707 6decb8811d30
parent 706 84e2e4649b48
child 708 587e97d144a0
tuned
Quot/Examples/LarryDatatype.thy file | annotate | diff | comparison | revisions 
--- 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"
nominal2