The name bex_conj_distrib was WRONG
authorpaulson
Fri, 06 Jun 1997 13:26:41 +0200
changeset 3426 9aa5864a7eea
parent 3425 fc4ca570d185
child 3427 e7cef2081106
The name bex_conj_distrib was WRONG
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;