src/HOL/MicroJava/BV/BVExample.thy
changeset 14045 a34d89ce6097
parent 13727 4ab8d49ab981
child 15045 d59f7e2e18d3
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon May 26 11:42:41 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon May 26 18:36:15 2003 +0200
     1.3 @@ -186,6 +186,7 @@
     1.4  text {*
     1.5    The program is structurally wellformed:
     1.6  *}
     1.7 +
     1.8  lemma wf_struct:
     1.9    "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
    1.10  proof -
    1.11 @@ -223,7 +224,8 @@
    1.12      apply (auto simp add: name_defs distinct_classes distinct_fields)
    1.13      done       
    1.14    ultimately
    1.15 -  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
    1.16 +  show ?thesis 
    1.17 +    by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
    1.18  qed
    1.19  
    1.20  section "Welltypings"