equal
deleted
inserted
replaced
1 |
1 |
2 header {* Syntactic classes *} |
2 header {* Syntactic classes *} |
3 |
3 |
4 theory Product = Main: |
4 theory Product imports Main begin |
5 |
5 |
6 text {* |
6 text {* |
7 \medskip\noindent There is still a feature of Isabelle's type system |
7 \medskip\noindent There is still a feature of Isabelle's type system |
8 left that we have not yet discussed. When declaring polymorphic |
8 left that we have not yet discussed. When declaring polymorphic |
9 constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>} |
9 constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>} |