diff -r 2d21fd8114af -r b2231990b059 Quot/Examples/LFex.thy --- a/Quot/Examples/LFex.thy Mon Dec 21 23:13:40 2009 +0100 +++ b/Quot/Examples/LFex.thy Tue Dec 22 07:28:09 2009 +0100 @@ -277,6 +277,7 @@ using a0 a1 a2 a3 a4 a5 a6 a7 a8 *) + lemma "\P TYP; \ty name kind. \Q ty; P kind\ \ P (KPI ty name kind); \id. Q (TCONST id);