Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hilbert_Choice.thy
changeset 18389 8352b1d3b639
parent 17893 aef5a6d11c2a
child 21020 9af9ceb16d58 
--- a/src/HOL/Hilbert_Choice.thy	Tue Dec 13 10:39:32 2005 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Tue Dec 13 15:27:43 2005 +0100
@@ -458,6 +458,7 @@
   and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
   and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
     -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
+  and meson_not_refl_disj_D: "x ~= x | P ==> P"
   by fast+
isabelle