equal
deleted
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 |