diff -r 58abc09d6f9c -r ea84c1a0a23c Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Mar 29 18:12:54 2010 +0200
+++ b/Paper/Paper.thy	Mon Mar 29 22:26:19 2010 +0200
@@ -394,10 +394,9 @@
   \caption{The term-language of System @{text "F\<^isub>C"}
   \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
   version of the term-language we made a modification by separating the
-  grammars for type and coercion kinds, as well as types and coercion
-  types. For this paper the interesting term-constructor is @{text "\<CASE>"}
-  involving the binding of multiple type-, coercion- and term-variables from
-  patterns.\label{corehas}}
+  grammars for type and coercion kinds, as well as for types and coercion
+  types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+  which binds multiple type-, coercion- and term-variables.\label{corehas}}
   \end{figure}
 *}
 
@@ -431,7 +430,7 @@
   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
   operation is defined by induction over the type-hierarchy, for example as follows 
   for products, lists, sets, functions and booleans (see \cite{HuffmanUrban10}):
-  
+  %
   \begin{equation}
   \mbox{\begin{tabular}{@ {}cc@ {}}
   \begin{tabular}{@ {}l@ {}}
@@ -1145,6 +1144,76 @@
 
 section {* Examples *}
 
+text {*
+
+  \begin{figure}
+  \begin{boxedminipage}{\linewidth}
+  \small
+  \begin{tabular}{l}
+  \isacommand{atom\_decl}~@{text "var"}\\
+  \isacommand{atom\_decl}~@{text "cvar"}\\
+  \isacommand{atom\_decl}~@{text "tvar"}\\[1mm]
+  \isacommand{nominal\_datatype}~@{text "tkind ="}\\
+  \phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ 
+  \isacommand{and}~@{text "ckind ="}\\
+  \phantom{$|$}~@{text "CKSim ty ty"}\\
+  \isacommand{and}~@{text "ty ="}\\
+  \phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+  $|$~@{text "TFun string ty_list"}~%
+  $|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+  $|$~@{text "TArr ckind ty"}\\
+  \isacommand{and}~@{text "ty_lst ="}\\
+  \phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+  \isacommand{and}~@{text "cty ="}\\
+  \phantom{$|$}~@{text "CVar cvar"}~%
+  $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+  $|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+  $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+  $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+  $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+  \isacommand{and}~@{text "co_lst ="}\\
+  \phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+  \isacommand{and}~@{text "trm ="}\\
+  \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
+  $|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+  $|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+  $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+  $|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+  $|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\
+  $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+  \isacommand{and}~@{text "assoc_lst ="}\\
+  \phantom{$|$}~@{text ANil}~%
+  $|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+  \isacommand{and}~@{text "pat ="}\\
+  \phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+  \isacommand{and}~@{text "vt_lst ="}\\
+  \phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+  \isacommand{and}~@{text "tvtk_lst ="}\\
+  \phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+  \isacommand{and}~@{text "tvck_lst ="}\\ 
+  \phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+  \isacommand{binder}\\
+  @{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
+  @{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+  @{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
+  @{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
+  \isacommand{where}\\
+  \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
+  $|$~@{text "bv1 VTNil = []"}\\
+  $|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
+  $|$~@{text "bv2 TVTKNil = []"}\\
+  $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
+  $|$~@{text "bv3 TVCKNil = []"}\\
+  $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
+  \end{tabular}
+  \end{boxedminipage}
+  \caption{\label{nominalcorehas}}
+  \end{figure}
+*}
+
+
+
+
 section {* Adequacy *}
 
 section {* Related Work *}
@@ -1181,7 +1250,9 @@
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
   also for patiently explaining some of the finer points about the abstract 
-  definitions and about the implementation of the Ott-tool.
+  definitions and about the implementation of the Ott-tool. We
+  also thank Stephanie Weirich for suggesting to separate the subgrammars
+  of kinds and types in our Core-Haskell example.
 
   Lookup: Merlin paper by James Cheney; Mark Shinwell PhD