# HG changeset patch
# User paulson
# Date 865596401 -7200
# Node ID 9aa5864a7eea3da46c85151d09d186f69c59df8c
# Parent  fc4ca570d1850331b702a0c0701523738de4e80f
The name bex_conj_distrib was WRONG

diff -r fc4ca570d185 -r 9aa5864a7eea src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jun 06 12:48:21 1997 +0200
+++ b/src/HOL/equalities.ML	Fri Jun 06 13:26:41 1997 +0200
@@ -699,7 +699,7 @@
      "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
      "(EX x:Collect Q. P x) = (EX x. Q x & P x)"];
 
-val bex_conj_distrib = 
+val bex_disj_distrib = 
     prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
 
 end;