diff --git a/grammar.ott b/grammar.ott
index 7751a14ceaee1a322f42dab85a67e95ca51250af..4d4b3f4d49f46dfd66dc5c2441dc7f60023fbd1a 100644
--- a/grammar.ott
+++ b/grammar.ott
@@ -123,7 +123,7 @@ G {{ tex \Gamma }}, Gt {{ tex \Gamma_t }} :: 'TyEnv_' ::= {{ com Type environmen
 | tv : type                    :: :: TyVar      {{ com Type variable binding }}
 | < tv : type >                :: M :: TyVars
   {{ tex \overline{ [[tv]] : [[type]] } }}
-| ( G )                        ::  :: Parens    {{ com Grouping }}
+| ( G )                        :: M :: Parens    {{ com Grouping }}
   {{ tex [[G]] }}
 | Giminus_one                  :: M  :: GIHack
 
@@ -178,7 +178,6 @@ terminals :: 'terminals_' ::=
 | ftv                            ::   :: ftv        {{ tex \mathit{ftv}\! }}
 | #                              ::   :: fresh      {{ tex \mathrel{\#} }}
 | @                              ::   :: at         {{ tex \at }}
-| isTV                           ::   :: isTV       {{ tex \mathit{isInternalTypeVar}\! }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -195,7 +194,6 @@ formula :: formula_ ::=
 |  obj1 = obj2                       ::   :: objeq
 |  < formula >                       ::   :: overline
    {{ tex \overline{[[formula]]} }}
-|  isTV ( t )                        ::   :: isTV
 
 % | x : t \in G                      ::   :: ctx_in
 %   {{ tex [[x]] : [[t]] \in [[G]] }}
diff --git a/haskell.mng b/haskell.mng
index 5bc484a56fabb77d033b68b4d3a9de02240b2892..bc2708fc3faf051fbe56e3706af03475a1cbcc45 100644
--- a/haskell.mng
+++ b/haskell.mng
@@ -3,6 +3,7 @@
 \usepackage[supertabular,implicitLineBreakHack]{ottalt}
 \usepackage[dvipsnames]{xcolor}
 \usepackage{amsmath}
+\usepackage{amssymb}
 \usepackage{fullpage}
 
 \inputott{ott.tex}
@@ -14,10 +15,31 @@
 \newcommand{\varid}[1]{\textcolor{Sepia}{\id{#1}}}
 
 
+\renewcommand\ottaltinferrule[4]{
+  \inferrule*[narrower=0.3,right=#1,#2]
+    {#3}
+    {#4}
+}
+
+
 \begin{document}
 
+\section{Metavariables}
+
+\ottmetavars
+
+\section{Grammar}
+
 \nonterms{prog,CL,v,e,p,sg,Q,tv,theta,t,G}
 
-\drules
+\section{Typing rules}
+
+\drules[E]{$[[G |- e : t]]$}{Expressions}{VarCon,Eq,App,Abs,Case,Let}
+
+Abstract judgments $[[G ||- Q]]$ denotes entailment and $[[G ||- sg1 <= sg2]]$ denotes
+subtyping ($[[sg1]]$ is more general than $[[sg2]]$).
+
+\drules[P]{$[[G |-p p : sg => G']]$}{Patterns}{Var,Con,Syn,Sig}
+\drules[Ps]{$[[G |-p* </ pi : sgi // i /> => G']]$}{Pattern sequences}{PatSeq}
 
 \end{document}
diff --git a/rules.ott b/rules.ott
index b1d16a3e1ebcd504e88235d95ae72dd9eca92140..6ebda6b49948a0bbfd6d037b9ad98711a741535d 100644
--- a/rules.ott
+++ b/rules.ott
@@ -9,30 +9,27 @@ by
 isTyVar ( a )
 
 defn
-G |- e : t :: :: Ty :: '' {{ com Expression typing }}
+G |- e : t :: :: Ty :: 'E_' {{ com Expression typing }}
 by
 
-(v : forall tvs . u) in G
------------- :: VarCon
-G |- v : [<tv |-> t>]u
-
 (v : forall as . Q => u) in G
 G ||- [< a |-> t >]Q
--------------------------- :: VarConQ
+-------------------------- :: VarCon
 G |- v : [< a |-> t >] u
 
-(P : forall as. Qr => forall bs. Qp => u) in G
-theta = [< a |-> t >][< b |-> t' >]
-G ||- theta(Qr /\ Qp)
------------------------- :: Syn
-G |- P : theta(u)
+% (P : forall as. Qr => forall bs. Qp => u) in G
+% theta = [< a |-> t >][< b |-> t' >]
+% G ||- theta(Qr /\ Qp)
+% ------------------------ :: Syn
+% G |- P : theta(u)
 
 G |- e : t1
 G ||- t1 ~ t2
 --------------------------------- :: Eq
 G |- e : t2
 
-G |- e1 : t1 -> t2 //   G |- e2 : t2
+G |- e1 : t1 -> t2
+G |- e2 : t2
 --------------------------------- :: App
 G |- e1 e2 : t2
 
@@ -40,29 +37,17 @@ G, (x : t1) |- e : t2
 --------------------------------- :: Abs
 G |- \x.e : t1 -> t2
 
-G |- e : u  //  </ G |-p pi : u => Gi'  // Gi' |- ei : t // i />
---------------------------------- :: Case
-G |- case e of {</ pi -> ei // i />} : t
-
 </ G |-p pi : u => Gi'  // Gi' |- ei : t // i />
-G |- e : u  //  ftv(t) (= dom(G)
---------------------------------- :: CaseTv
+G |- e : u
+ftv(t) (= dom(G)
+--------------------------------- :: Case
 G |- case e of {</ pi -> ei // i />} : t
 
-G |- e : u // cs = ftv(u)
-G, x : forall cs.u |- e2 : t
+sg = forall cs. Q => u
+ftv(sg) (= dom(G)
+G, <c : type>, Q  |- e : u
+G, x : sg |- e2 : t
 ----------------------------- :: Let
-G |- let x :: u = e in e2 : t
-
-G, <a : type> |- e : [<c |-> a>]u
-cs = ftv(u)      // as # dom(G)
-G, x : forall cs.u |- e2 : t
------------------------------ :: LetTv
-G |- let x :: u = e in e2 : t
-
-sg = forall cs. Q => u  // ftv(sg) (= dom(G)
-G, <c : type>, Q  |- e : u  // G, x : sg |- e2 : t
------------------------------ :: LetForall
 G |- let x :: sg = e in e2 : t
 
 defn
@@ -75,25 +60,18 @@ by
 
 
 defn
-G |-p p : sg => G' :: :: Pat :: 'Pat' {{ com Pattern typing }}
+G |-p p : sg => G' :: :: Pat :: 'P_' {{ com Pattern typing }}
 by
 
 -------------------------------- :: Var
 G |-p x : sg => G, (x : sg)
 
-(K : forall </ ai // i /> . </ sgk // k /> -> T </ ai // i />) in G     //      G |-p* </ pk : [</ ai |-> ti // i />]sgk // k /> => G'
--------------------------------- :: Con98
-G |-p K </ pk // k /> : T </ ti // i /> => G'
-
-(K : forall as. Q  => </ sgi // i /> -> T </ uj // j />) in G   // as # dom(G)
-G, < a : type >, (</ uj ~ tj // j />), Q |-p* </ pi : sgi // i /> => G'
--------------------------------- :: Con
-G |-p K </ pi // i /> : T </ tj // j /> => G'
-
 (P : forall </ ai // i />. Qr => forall </ bj // j />. Qp => </ sgk // k /> -> u) in G
-G' = G, (</ ai : type // i />), (</ ai ~ u'i // i />)  // </ ai // i /> # dom(G)
+G' = G, (</ ai : type // i />), (</ ai ~ u'i // i />)
+</ ai // i /> # dom(G)
 G' ||- (u ~ t) /\ Qr
-</ cl // l /> = ftv(</ t'i // i />,</ t''j // j />) \ dom(G)  // </ bj // j /> # dom(G)
+</ cl // l /> = ftv(</ t'i // i />,</ t''j // j />) \ dom(G)
+</ bj // j /> # dom(G)
 G'' = G',(</ bj : type // j />),(</ cl : type // l />),(</ cl ~ b'l // l />),Qp
 </ G'' ||- t'i ~ ai // i />
 </ G'' ||- t''j ~ bj // j />
@@ -104,29 +82,25 @@ G |-p P </ @ t'i // i /> </ @ t''j // j /> </ pk // k /> : t => G'''
 
 
 (K : forall </ aj // j /> . Q  => </ sgk // k /> -> T </ ui // i />) in G
-</ cl // l /> = ftv(</ t'j // j />) \ dom(G)  //  </ aj // j /> # dom(G)
+</ cl // l /> = ftv(</ t'j // j />) \ dom(G)
+</ aj // j /> # dom(G)
 G' = G,(</ aj : type // j />),(</ cl : type // l />),(</ cl ~ t''l // l />),(</ ui ~ ti // i />),Q
-</ G' ||- t'j ~ aj // j /> // </ isTV(t''l) // l />
+</ G' ||- t'j ~ aj // j />
 G' |-p* </ pk : sgk // k /> => G''
--------------------------------- :: ConTyApp
+-------------------------------- :: Con
 G |-p K </ @ t'j // j /> </ pk // k /> : T </ ti // i /> => G''
 
-
-
-ftv(sg') = emptyset //  G ||- sg <= sg'  //  G |-p p : sg' => G'
+cs = ftv(sg') \ dom(G)
+G' = G, <c : type>, < c ~ t >
+G' ||- sg <= sg'
+G' |-p p : sg' => G''
 -------------------------------- :: Sig
-G |-p (p :: sg') : sg => G'
-
-cs = ftv(sg') \ dom(G)  //  G' = G, <c : type>, < c ~ t >
-< isTV(t) > 
-G' ||- sg <= sg' // G' |-p p : sg' => G''
--------------------------------- :: SigTv
 G |-p (p :: sg') : sg => G''
 
 
 
 defn
-G |-p* </ pi : sgi // i />  => G' :: :: PatSeq :: '' {{ com Pattern squence typing }}
+G |-p* </ pi : sgi // i />  => G' :: :: PatSeq :: 'Ps_' {{ com Pattern squence typing }}
 by
 
 % help, how do I typeset that with G_{i-1}
@@ -135,11 +109,11 @@ by
 G0 |-p*  </ pi : sgi // i IN 1 .. n />  => Gn
 
 
-defn
-G |-sb* e <= sg :: :: Check :: '' {{ com Checking against specified polytypes }}
-  {{ tex [[G]] [[|-sb*]] [[e]] \Leftarrow [[sg]] }}
-by
+% defn
+% G |-sb* e <= sg :: :: Check :: '' {{ com Checking against specified polytypes }}
+%   {{ tex [[G]] [[|-sb*]] [[e]] \Leftarrow [[sg]] }}
+% by
 
-G, c : type |-sb* e <= [a |-> c]sg
---------------------------------- :: SB_DTyAbs
-G |-sb* \ @c . e <= forall a. sg
+% G, c : type |-sb* e <= [a |-> c]sg
+% --------------------------------- :: SB_DTyAbs
+% G |-sb* \ @c . e <= forall a. sg