src/Doc/ProgProve/Types_and_funs.thy
 changeset 51465 c5c466706549 parent 51393 df0f306f030f child 52045 90cd3c53a887
equal inserted replaced
51464:6cd801fabb34 51465:c5c466706549
    14
    14
    15 text{*
    15 text{*
    16 Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
    16 Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
    17
    17
    18 \subsection{Datatypes}
    18 \subsection{Datatypes}

    19 \label{sec:datatypes}
    19
    20
    20 The general form of a datatype definition looks like this:
    21 The general form of a datatype definition looks like this:
    21 \begin{quote}
    22 \begin{quote}
    22 \begin{tabular}{@ {}rclcll}
    23 \begin{tabular}{@ {}rclcll}
    23 \isacom{datatype} @{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}
    24 \isacom{datatype} @{text "('a\<^isub>1,\<dots>,'a\<^isub>n)t"}