equal
deleted
inserted
replaced
1 (*<*)theory Advanced imports Even begin |
1 (*<*)theory Advanced imports Even begin(*>*) |
2 ML_file \<open>../../antiquote_setup.ML\<close> |
|
3 (*>*) |
|
4 |
2 |
5 text \<open> |
3 text \<open> |
6 The premises of introduction rules may contain universal quantifiers and |
4 The premises of introduction rules may contain universal quantifiers and |
7 monotone functions. A universal quantifier lets the rule |
5 monotone functions. A universal quantifier lets the rule |
8 refer to any number of instances of |
6 refer to any number of instances of |