equal
deleted
inserted
replaced
819 apply (blast intro: order_less_trans) |
819 apply (blast intro: order_less_trans) |
820 done |
820 done |
821 |
821 |
822 lemma le_min_iff_conj [simp]: |
822 lemma le_min_iff_conj [simp]: |
823 "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)" |
823 "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)" |
824 -- {* @{text "[iff]"} screws up a Q{text blast} in MiniML *} |
824 -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *} |
825 apply (simp add: min_def) |
825 apply (simp add: min_def) |
826 apply (insert linorder_linear) |
826 apply (insert linorder_linear) |
827 apply (blast intro: order_trans) |
827 apply (blast intro: order_trans) |
828 done |
828 done |
829 |
829 |