equal
deleted
inserted
replaced
1 (*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin |
1 (*<*)theory Advanced imports Even begin |
2 setup {* Antiquote_Setup.setup *} |
2 ML_file "../../antiquote_setup.ML" |
|
3 setup Antiquote_Setup.setup |
3 (*>*) |
4 (*>*) |
4 |
5 |
5 text {* |
6 text {* |
6 The premises of introduction rules may contain universal quantifiers and |
7 The premises of introduction rules may contain universal quantifiers and |
7 monotone functions. A universal quantifier lets the rule |
8 monotone functions. A universal quantifier lets the rule |