changeset 43564 9864182c6bad parent 40406 313a24b66a8d child 46192 93eaaacc1955
equal inserted replaced
    12 {\isafoldtheory}%
    12 {\isafoldtheory}%
    13 %
    13 %
    14 \isadelimtheory
    14 \isadelimtheory
    15 %
    15 %
    16 \endisadelimtheory
    16 \endisadelimtheory

    17 %

    18 \isadelimML

    19 %

    20 \endisadelimML

    21 %

    22 \isatagML

    23 %

    24 \endisatagML

    25 {\isafoldML}%

    26 %

    27 \isadelimML

    28 %

    29 \endisadelimML
    17 %
    30 %
    18 \begin{isamarkuptext}%
    31 \begin{isamarkuptext}%
    19 The premises of introduction rules may contain universal quantifiers and
    32 The premises of introduction rules may contain universal quantifiers and
    20 monotone functions.  A universal quantifier lets the rule
    33 monotone functions.  A universal quantifier lets the rule
    21 refer to any number of instances of
    34 refer to any number of instances of