equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Product}% |
3 \def\isabellecontext{Product}% |
4 % |
4 % |
5 \isamarkupheader{Syntactic classes} |
5 \isamarkupheader{Syntactic classes% |
|
6 } |
6 \isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}% |
7 \isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}% |
7 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
8 \medskip\noindent There is still a feature of Isabelle's type system |
9 \medskip\noindent There is still a feature of Isabelle's type system |
9 left that we have not yet discussed. When declaring polymorphic |
10 left that we have not yet discussed. When declaring polymorphic |
10 constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} |
11 constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} |