equal
deleted
inserted
replaced
2426 by simp |
2426 by simp |
2427 |
2427 |
2428 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)" |
2428 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)" |
2429 by auto |
2429 by auto |
2430 |
2430 |
2431 |
2431 use "Tools/function_package/lexicographic_order.ML" |
|
2432 setup {* LexicographicOrder.setup *} |
2432 |
2433 |
2433 subsubsection{*Lifting a Relation on List Elements to the Lists*} |
2434 subsubsection{*Lifting a Relation on List Elements to the Lists*} |
2434 |
2435 |
2435 consts listrel :: "('a * 'a)set => ('a list * 'a list)set" |
2436 consts listrel :: "('a * 'a)set => ('a list * 'a list)set" |
2436 |
2437 |