equal
deleted
inserted
replaced
369 lemma appl_methds_foo_Base: |
369 lemma appl_methds_foo_Base: |
370 "appl_methds tprg Base (foo, [NT]) = |
370 "appl_methds tprg Base (foo, [NT]) = |
371 {((Class Base, Class Base), [Class Base])}" |
371 {((Class Base, Class Base), [Class Base])}" |
372 apply (unfold appl_methds_def) |
372 apply (unfold appl_methds_def) |
373 apply (simp (no_asm)) |
373 apply (simp (no_asm)) |
374 apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base") |
|
375 apply (auto simp add: map_of_Cons foo_Base_def) |
|
376 done |
374 done |
377 |
375 |
378 lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) = |
376 lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) = |
379 {((Class Base, Class Base), [Class Base])}" |
377 {((Class Base, Class Base), [Class Base])}" |
380 apply (unfold max_spec_def) |
378 apply (unfold max_spec_def) |