equal
deleted
inserted
replaced
1 |
1 |
2 header {* Basic group theory *} |
2 header {* Basic group theory *} |
3 |
3 |
4 theory Group = Main: |
4 theory Group imports Main begin |
5 |
5 |
6 text {* |
6 text {* |
7 \medskip\noindent The meta-level type system of Isabelle supports |
7 \medskip\noindent The meta-level type system of Isabelle supports |
8 \emph{intersections} and \emph{inclusions} of type classes. These |
8 \emph{intersections} and \emph{inclusions} of type classes. These |
9 directly correspond to intersections and inclusions of type |
9 directly correspond to intersections and inclusions of type |