Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Used locale interpretations everywhere. -> lemma had new name
authornipkow
Wed, 20 Apr 2005 17:19:42 +0200
changeset 15781 70d559802ae3
parent 15780 6744bba5561d
child 15782 a1863ea9052b
Used locale interpretations everywhere. -> lemma had new name
src/HOL/MicroJava/Comp/CorrCompTp.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Apr 20 17:19:18 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Apr 20 17:19:42 2005 +0200
@@ -908,7 +908,7 @@
 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 del: max_assoc add: max_assoc [THEN sym])
+by (simp add: AC_max.assoc [THEN sym])
 
   (* ******************************************************************* *)
isabelle