| changeset 9559 | 1f99296758c2 |
| parent 9549 | 40d64cb4f4e6 |
| child 9757 | 1024a2d80ac0 |
--- a/src/HOL/MicroJava/BV/BVSpec.thy Tue Aug 08 16:57:44 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Wed Aug 09 11:53:00 2000 +0200 @@ -36,6 +36,8 @@ wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (phi C sig)) G" + + lemma wt_jvm_progD: "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)" by (unfold wt_jvm_prog_def, blast)