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/BV/LBVJVM.thy
changeset 13601 fd3e3d6b37b2
parent 13224 6f0928a942d1
child 14045 a34d89ce6097 
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Mon Sep 30 16:14:02 2002 +0200
@@ -215,7 +215,7 @@
     ck_types:   "check_types G mxs ?mxr ?phi" and
     wt_start:   "wt_start G C pTs mxl phi" and
     app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
-    by (simp add: wt_method_def2)
+    by (simp (asm_lr) add: wt_method_def2)
   
   have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI)
   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
isabelle