equal
deleted
inserted
replaced
254 (flatten (int_unlift ctxt th) handle THM _ => th) |
254 (flatten (int_unlift ctxt th) handle THM _ => th) |
255 | _ => th |
255 | _ => th |
256 \<close> |
256 \<close> |
257 |
257 |
258 attribute_setup int_unlift = |
258 attribute_setup int_unlift = |
259 \<open>Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\<close> |
259 \<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close> |
260 attribute_setup int_rewrite = |
260 attribute_setup int_rewrite = |
261 \<open>Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\<close> |
261 \<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close> |
262 attribute_setup flatten = \<open>Scan.succeed (Thm.rule_attribute (K flatten))\<close> |
262 attribute_setup flatten = |
|
263 \<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close> |
263 attribute_setup int_use = |
264 attribute_setup int_use = |
264 \<open>Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\<close> |
265 \<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close> |
265 |
266 |
266 lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)" |
267 lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)" |
267 by (simp add: Valid_def) |
268 by (simp add: Valid_def) |
268 |
269 |
269 lemma Not_Rex: "\<turnstile> (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)" |
270 lemma Not_Rex: "\<turnstile> (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)" |