src/HOL/Hilbert_Choice.thy
changeset 18389 8352b1d3b639
parent 17893 aef5a6d11c2a
child 21020 9af9ceb16d58
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Dec 13 10:39:32 2005 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Dec 13 15:27:43 2005 +0100
     1.3 @@ -458,6 +458,7 @@
     1.4    and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
     1.5    and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
     1.6      -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
     1.7 +  and meson_not_refl_disj_D: "x ~= x | P ==> P"
     1.8    by fast+
     1.9  
    1.10