equal
deleted
inserted
replaced
26 apply clarsimp |
26 apply clarsimp |
27 apply (blast dest: monoD) |
27 apply (blast dest: monoD) |
28 apply (fastsimp intro!: lfp_lowerbound) |
28 apply (fastsimp intro!: lfp_lowerbound) |
29 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) |
29 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) |
30 apply (clarsimp simp add: finite_psubset_def order_less_le) |
30 apply (clarsimp simp add: finite_psubset_def order_less_le) |
31 apply (blast intro!: finite_Diff dest: monoD) |
31 apply (blast dest: monoD) |
32 done |
32 done |
33 |
33 |
34 |
34 |
35 subsection {* Example *} |
35 subsection {* Example *} |
36 |
36 |