# HG changeset patch
# User nipkow
# Date 1114096943 -7200
# Node ID e9b7e210ad2acc3843b00996e7f141eb238fc10e
# Parent  446ec11266be9aefcb9b6e8981b4fe4559c96809
fix

diff -r 446ec11266be -r e9b7e210ad2a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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