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