Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/Comp/CorrCompTp.thy
changeset 55584 a879f14b6f95
parent 55524 f41ef840f09d
child 56073 29e308b56d23 
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 19 22:02:23 2014 +1100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Feb 19 16:32:37 2014 +0100
@@ -1394,7 +1394,7 @@
 
   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
     apply (rule max_of_list_sublist)
-    apply (simp (no_asm_simp) only: set_append set.simps list.map) apply blast
+    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
   apply (simp (no_asm_simp))
   apply simp                    (* subgoal bc3 = [] *)
   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
@@ -1421,7 +1421,7 @@
      (* (some) preconditions of  wt_instr_offset *)
   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
   apply (rule max_of_list_sublist)
-    apply (simp (no_asm_simp) only: set_append set.simps list.map) apply blast
+    apply (simp (no_asm_simp) only: set_append set_simps list.map) apply blast
   apply (simp (no_asm_simp))
 
 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
isabelle