| changeset 67613 | ce654b0e6d69 |
| parent 67487 | b4e65cd6974a |
| child 69605 | a96320074298 |
--- a/src/HOL/Fun_Def.thy Tue Feb 13 14:24:50 2018 +0100 +++ b/src/HOL/Fun_Def.thy Thu Feb 15 12:11:00 2018 +0100 @@ -198,7 +198,7 @@ subsection \<open>Concrete orders for SCNP termination proofs\<close> definition "pair_less = less_than <*lex*> less_than" -definition "pair_leq = pair_less^=" +definition "pair_leq = pair_less\<^sup>=" definition "max_strict = max_ext pair_less" definition "max_weak = max_ext pair_leq \<union> {({}, {})}" definition "min_strict = min_ext pair_less"