equal
deleted
inserted
replaced
391 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1) |
391 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1) |
392 done |
392 done |
393 |
393 |
394 lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C" |
394 lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C" |
395 apply (erule implmt.induct) |
395 apply (erule implmt.induct) |
396 apply (blast dest: implmt1D subcls1D)+ |
396 apply (auto dest: implmt1D subcls1D) |
397 done |
397 done |
398 |
398 |
399 |
399 |
400 section "widening relation" |
400 section "widening relation" |
401 |
401 |