equal
deleted
inserted
replaced
37 instantiation rlam :: fs |
37 instantiation rlam :: fs |
38 begin |
38 begin |
39 |
39 |
40 lemma neg_conj: |
40 lemma neg_conj: |
41 "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)" |
41 "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)" |
42 by simp |
|
43 |
|
44 lemma infinite_Un: |
|
45 "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
46 by simp |
42 by simp |
47 |
43 |
48 instance |
44 instance |
49 apply default |
45 apply default |
50 apply(induct_tac x) |
46 apply(induct_tac x) |