| 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 {*