# HG changeset patch # User wenzelm # Date 1013802079 -3600 # Node ID a0b2acb7d6fac5db882bb452c0f5d94c001234d3 # Parent 92af5c3a10fb7487ca0f398cc684f8dd66f9086e tuned; diff -r 92af5c3a10fb -r a0b2acb7d6fa src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Feb 15 12:07:27 2002 +0100 +++ b/src/HOL/HOL.thy Fri Feb 15 20:41:19 2002 +0100 @@ -821,7 +821,7 @@ lemma le_min_iff_conj [simp]: "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)" - -- {* @{text "[iff]"} screws up a Q{text blast} in MiniML *} + -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *} apply (simp add: min_def) apply (insert linorder_linear) apply (blast intro: order_trans)