Lines Matching refs:ASSOC
103 #let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3";;
104 ASSOC = |- (t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3
152 #REWR_CONV ASSOC "(A /\ B) /\ C";;
155 #REWR_CONV ASSOC "A /\ (B /\ C)";;
256 \ml{REWR\_CONV\ ASSOC}
295 #REWR_CONV ASSOC ex1;;
298 #TOP_DEPTH_CONV (REWR_CONV ASSOC) ex1;;
360 # TOP_DEPTH_CONV(REWR_CONV ASSOC) THENC
414 let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3"
430 TOP_DEPTH_CONV(REWR_CONV ASSOC) THENC
1309 AC_CANON_CONV(ASSOC,SYM1)