# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269346022 -3600
# Node ID 98b53cd05deb01042c760c124e41384a7f6ddf79
# Parent  c8c9b3b7189a0f169de744be141967498cb5937c
more tuning

diff -r c8c9b3b7189a -r 98b53cd05deb Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 23 13:03:42 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 13:07:02 2010 +0100
@@ -527,7 +527,8 @@
   collection of (possibly mutual recursive) type declarations, say
   $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
   collection of associated binding function declarations, say
-  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are written as follows:
+  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically 
+  written as follows:
 
   \begin{center}
   \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}