440   \caption{The System @{text "F\<^isub>C"}

   440   \caption{The System @{text "F\<^isub>C"}

   441   \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this

   441   \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this

   442   version of @{text "F\<^isub>C"} we made a modification by separating the

   442   version of @{text "F\<^isub>C"} we made a modification by separating the

   443   grammars for type kinds and coercion kinds, as well as for types and coercion

   443   grammars for type kinds and coercion kinds, as well as for types and coercion

   444   types. For this paper the interesting term-constructor is @{text "\<CASE>"},

   444   types. For this paper the interesting term-constructor is @{text "\<CASE>"},

   446   \end{figure}

   446   \end{figure}

   447 *}

   447 *}

   448 

   448 

   449 section {* A Short Review of the Nominal Logic Work *}

   449 section {* A Short Review of the Nominal Logic Work *}

   450 

   450 

  2628   definitions to equivariant functions (for them we can provide more

  2628   definitions to equivariant functions (for them we can provide more

  2629   automation).

  2629   automation).

  2630 

  2630 

  2631   There are some restrictions we imposed in this paper that we would like to lift in

  2631   There are some restrictions we imposed in this paper that we would like to lift in

  2632   future work. One is the exclusion of nested datatype definitions. Nested

  2632   future work. One is the exclusion of nested datatype definitions. Nested

  2634   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded

  2634   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded

  2635   version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To

  2635   version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To

  2636   achieve this, we need more clever implementation than we have 

  2636   achieve this, we need more clever implementation than we have 

  2637   at the moment. However, really lifting this restriction will involve major

  2637   at the moment. However, really lifting this restriction will involve major

  2638   work on the underlying datatype package of Isabelle/HOL.

  2638   work on the underlying datatype package of Isabelle/HOL.

  2660   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many

  2660   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many

  2661   discussions about Nominal Isabelle. We thank Peter Sewell for making the

  2661   discussions about Nominal Isabelle. We thank Peter Sewell for making the

  2662   informal notes \cite{SewellBestiary} available to us and also for patiently

  2662   informal notes \cite{SewellBestiary} available to us and also for patiently

  2663   explaining some of the finer points of the Ott-tool.  Stephanie Weirich

  2663   explaining some of the finer points of the Ott-tool.  Stephanie Weirich

  2664   suggested to separate the subgrammars of kinds and types in our Core-Haskell

  2664   suggested to separate the subgrammars of kinds and types in our Core-Haskell

  2667 *}

  2667 *}

  2668 

  2668 

  2669 

  2669 

  2670 (*<*)

  2670 (*<*)

  2671 end

  2671 end