equal
deleted
inserted
replaced
83 |
83 |
84 end |
84 end |
85 |
85 |
86 lemma eval_INFI [simp]: |
86 lemma eval_INFI [simp]: |
87 "eval (INFI A f) = INFI A (eval \<circ> f)" |
87 "eval (INFI A f) = INFI A (eval \<circ> f)" |
88 by (simp only: INF_def eval_Inf image_compose) |
88 by (simp only: INF_def eval_Inf image_comp) |
89 |
89 |
90 lemma eval_SUPR [simp]: |
90 lemma eval_SUPR [simp]: |
91 "eval (SUPR A f) = SUPR A (eval \<circ> f)" |
91 "eval (SUPR A f) = SUPR A (eval \<circ> f)" |
92 by (simp only: SUP_def eval_Sup image_compose) |
92 by (simp only: SUP_def eval_Sup image_comp) |
93 |
93 |
94 instantiation pred :: (type) complete_boolean_algebra |
94 instantiation pred :: (type) complete_boolean_algebra |
95 begin |
95 begin |
96 |
96 |
97 definition |
97 definition |