equal
deleted
inserted
replaced
16 lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" |
16 lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" |
17 by blast |
17 by blast |
18 |
18 |
19 (*FIXME: move to ZF.thy or even to FOL.thy??*) |
19 (*FIXME: move to ZF.thy or even to FOL.thy??*) |
20 lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)" |
20 lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)" |
21 by blast |
|
22 |
|
23 (*FIXME: move to upair once it's Isar format*) |
|
24 lemma the_eq_trivial [simp]: "(THE x. x = a) = a" |
|
25 by blast |
21 by blast |
26 |
22 |
27 (** Monotonicity of implications -- some could go to FOL **) |
23 (** Monotonicity of implications -- some could go to FOL **) |
28 |
24 |
29 lemma in_mono: "A<=B ==> x:A --> x:B" |
25 lemma in_mono: "A<=B ==> x:A --> x:B" |