The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
P ==> R.

--- a/simpdata.ML	Mon Jan 30 16:32:32 1995 +0100
+++ b/simpdata.ML	Wed Feb 01 17:17:35 1995 +0100
@@ -70,9 +70,6 @@
 val eq_sym_conv = prover "(x=y) = (y=x)";
 
 val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
-val conj_commute = prover "(P&Q) = (Q&P)";
-val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
-val conj_comms = [conj_commute, conj_left_commute];
 
 val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
  (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
@@ -93,12 +90,16 @@
 	 rtac (if_not_P RS ssubst) 1,
 	 REPEAT(fast_tac HOL_cs 1) ]);
 
+val if_bool_eq = prove_goal HOL.thy "if(P,Q,R) = ((P-->Q) & (~P-->R))"
+  (fn _ => [rtac expand_if 1]);
+
 infix addcongs;
 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
 
 val mksimps_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
-   ("All", [spec]), ("True", []), ("False", [])];
+   ("All", [spec]), ("True", []), ("False", []),
+   ("if", [if_bool_eq RS iffD1])];
 
 fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
 
@@ -151,3 +152,12 @@
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
 end;
+
+fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]);
+
+prove "conj_commute" "(P&Q) = (Q&P)";
+prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
+val conj_comms = [conj_commute, conj_left_commute];
+
+prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
+prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";