| changeset 15097 | b807858b97bd |
| parent 15076 | 4b3d280ef06a |
| child 15236 | f289e8ba2bb3 |
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Mon Aug 02 10:12:02 2004 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon Aug 02 10:15:37 2004 +0200 @@ -52,7 +52,7 @@ done theorem exec_all_refl: "exec_all G s s" -by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) ) +by (simp only: exec_all_def) theorem exec_instr_in_exec_all: