changeset 15792 | e9b7e210ad2a |
parent 15781 | 70d559802ae3 |
child 17778 | 93d7e524417a |
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Apr 21 17:22:17 2005 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Apr 21 17:22:23 2005 +0200 @@ -907,9 +907,6 @@ \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))" by (simp add: check_type_def states_lower) -lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y" -by (simp add: AC_max.assoc [THEN sym]) - (* ******************************************************************* *) constdefs