tuned;
authorwenzelm
Fri, 15 Feb 2002 20:41:19 +0100
changeset 12892 a0b2acb7d6fa
parent 12891 92af5c3a10fb
child 12893 cbb4dc5e6478
tuned;
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)