equal
deleted
inserted
replaced
171 by (simp add: flift2_def) |
171 by (simp add: flift2_def) |
172 |
172 |
173 lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>" |
173 lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>" |
174 by (erule lift_definedE, simp) |
174 by (erule lift_definedE, simp) |
175 |
175 |
|
176 lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)" |
|
177 by (cases x, simp_all) |
|
178 |
176 text {* |
179 text {* |
177 \medskip Extension of @{text cont_tac} and installation of simplifier. |
180 \medskip Extension of @{text cont_tac} and installation of simplifier. |
178 *} |
181 *} |
179 |
182 |
180 lemmas cont_lemmas_ext [simp] = |
183 lemmas cont_lemmas_ext [simp] = |