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 57816 d8bbb97689d3
parent 56154 f0a927235162
child 58263 6c907aad90ba 
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Aug 07 12:17:41 2014 +0200
@@ -1392,7 +1392,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 list.set list.map) apply blast
   apply (simp (no_asm_simp))
   apply simp                    (* subgoal bc3 = [] *)
   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
@@ -1419,7 +1419,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 list.set list.map) apply blast
   apply (simp (no_asm_simp))
 
 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
isabelle