equal
deleted
inserted
replaced
11 theory BNF_Util |
11 theory BNF_Util |
12 imports |
12 imports |
13 "../Ordinals_and_Cardinals/Cardinal_Arithmetic" |
13 "../Ordinals_and_Cardinals/Cardinal_Arithmetic" |
14 "~~/src/HOL/Library/Prefix_Order" |
14 "~~/src/HOL/Library/Prefix_Order" |
15 Equiv_Relations_More |
15 Equiv_Relations_More |
16 uses |
|
17 ("Tools/bnf_util.ML") |
|
18 begin |
16 begin |
19 |
17 |
20 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" |
18 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" |
21 by (erule iffI) (erule contrapos_pn) |
19 by (erule iffI) (erule contrapos_pn) |
22 |
20 |