src/HOL/ex/Landau.thy
changeset 36635 080b755377c0
parent 31381 b3a785a69538
child 36809 354b15d5b4ca
--- a/src/HOL/ex/Landau.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/ex/Landau.thy	Tue May 04 08:55:43 2010 +0200
@@ -187,7 +187,7 @@
 proof -
   interpret preorder_equiv less_eq_fun less_fun proof
   qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
-  show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
   show "preorder_equiv.equiv less_eq_fun = equiv_fun"
     by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
 qed