SPLICE_CONJ_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Partially normalize a conjunction.
DESCRIPTION
Normalize to right associativity a conjunction without recursing in the right conjunct.
FAILURE
Fails if the user-provided term is not a conjunction.
EXAMPLE
> SPLICE_CONJ_CONV ``(a1 /\ a2 /\ a3) /\ b /\ c``;
val it = |- (a1 /\ a2 /\ a3) /\ b /\ c <=> a1 /\ a2 /\ a3 /\ b /\ c: thm

> SPLICE_CONJ_CONV ``(a1 /\ a2) /\ (b1 /\ b2) /\ c``;
val it = |- (a1 /\ a2) /\ (b1 /\ b2) /\ c <=> a1 /\ a2 /\ (b1 /\ b2) /\ c: thm
HOL  Kananaskis-13