1.1 --- a/src/HOL/HOL.thy	Fri Feb 15 12:07:27 2002 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Feb 15 20:41:19 2002 +0100
     1.3 @@ -821,7 +821,7 @@
     1.4  
     1.5  lemma le_min_iff_conj [simp]:
     1.6      "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
     1.7 -    -- {* @{text "[iff]"} screws up a Q{text blast} in MiniML *}
     1.8 +    -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
     1.9    apply (simp add: min_def)
    1.10    apply (insert linorder_linear)
    1.11    apply (blast intro: order_trans)