equal
deleted
inserted
replaced
672 end" |
672 end" |
673 "m + n, m * n, m - n"} |
673 "m + n, m * n, m - n"} |
674 *} |
674 *} |
675 |
675 |
676 text {* |
676 text {* |
677 In this example we obtain three terms whose variables @{text m} and @{text |
677 In this example we obtain three terms (using @{ML_ind parse_term in Syntax}) whose |
678 n} are of type @{typ "nat"}. If you have only a single term, then @{ML |
678 variables @{text m} and @{text n} are of type @{typ "nat"}. If you have only |
|
679 a single term, then @{ML |
679 check_terms in Syntax} needs plumbing. This can be done with the function |
680 check_terms in Syntax} needs plumbing. This can be done with the function |
680 @{ML singleton}.\footnote{There is already a function @{ML check_term in |
681 @{ML singleton}.\footnote{There is already a function @{ML check_term in |
681 Syntax} in the Isabelle sources that is defined in terms of @{ML singleton} |
682 Syntax} in the Isabelle sources that is defined in terms of @{ML singleton} |
682 and @{ML check_terms in Syntax}.} For example |
683 and @{ML check_terms in Syntax}.} For example |
683 |
684 |