equal
deleted
inserted
replaced
145 definition |
145 definition |
146 approx_upper_pd_def: "approx = upper_pd.completion_approx" |
146 approx_upper_pd_def: "approx = upper_pd.completion_approx" |
147 |
147 |
148 instance |
148 instance |
149 apply (intro_classes, unfold approx_upper_pd_def) |
149 apply (intro_classes, unfold approx_upper_pd_def) |
150 apply (simp add: upper_pd.chain_completion_approx) |
150 apply (rule upper_pd.chain_completion_approx) |
151 apply (rule upper_pd.lub_completion_approx) |
151 apply (rule upper_pd.lub_completion_approx) |
152 apply (rule upper_pd.completion_approx_idem) |
152 apply (rule upper_pd.completion_approx_idem) |
153 apply (rule upper_pd.finite_fixes_completion_approx) |
153 apply (rule upper_pd.finite_fixes_completion_approx) |
154 done |
154 done |
155 |
155 |