src/HOL/MetisExamples/BT.thy
changeset 29511 7071b017cb35
parent 28592 824f8390aaa2
child 29782 02e76245e5af
--- a/src/HOL/MetisExamples/BT.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -84,7 +84,7 @@
 lemma depth_reflect: "depth (reflect t) = depth t"
   apply (induct t)
   apply (metis depth.simps(1) reflect.simps(1))
-  apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2))
+  apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2))
   done
 
 text {*