src/Doc/ProgProve/Types_and_funs.thy
changeset 51465 c5c466706549
parent 51393 df0f306f030f
child 52045 90cd3c53a887
equal deleted 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"}