| changeset 35274 | 1cb90bbbf45e |
| parent 32960 | 69916a850301 |
| child 39246 | 9e58f0499f57 |
--- a/src/HOL/UNITY/Comp/AllocBase.thy Mon Feb 22 09:15:11 2010 +0100 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Mon Feb 22 09:15:12 2010 +0100 @@ -58,9 +58,8 @@ apply (rule monoI) apply (unfold prefix_def) apply (erule genPrefix.induct, auto) -apply (simp add: union_le_mono) apply (erule order_trans) -apply (rule union_upper1) +apply simp done (** setsum **)