changeset 57 | 194d088c1511 |
parent 43 | 424c7b1489df |
child 62 | 32a83e3ad5a4 |
--- a/simpdata.ML Tue Mar 22 08:28:31 1994 +0100 +++ b/simpdata.ML Tue Mar 22 08:31:58 1994 +0100 @@ -69,6 +69,9 @@ in val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))"; +val conj_commute = prover "(P&Q) = (Q&P)"; +val conj_right_commute = prover "((P&Q)&R) = ((P&R)&Q)"; +val conj_ac = [conj_assoc RS sym, conj_commute, conj_right_commute]; val if_True = prove_goal HOL.thy "if(True,x,y) = x" (fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);