equal
deleted
inserted
replaced
196 |
196 |
197 |
197 |
198 subsection \<open>Concrete orders for SCNP termination proofs\<close> |
198 subsection \<open>Concrete orders for SCNP termination proofs\<close> |
199 |
199 |
200 definition "pair_less = less_than <*lex*> less_than" |
200 definition "pair_less = less_than <*lex*> less_than" |
201 definition "pair_leq = pair_less^=" |
201 definition "pair_leq = pair_less\<^sup>=" |
202 definition "max_strict = max_ext pair_less" |
202 definition "max_strict = max_ext pair_less" |
203 definition "max_weak = max_ext pair_leq \<union> {({}, {})}" |
203 definition "max_weak = max_ext pair_leq \<union> {({}, {})}" |
204 definition "min_strict = min_ext pair_less" |
204 definition "min_strict = min_ext pair_less" |
205 definition "min_weak = min_ext pair_leq \<union> {({}, {})}" |
205 definition "min_weak = min_ext pair_leq \<union> {({}, {})}" |
206 |
206 |