The conversion bool_EQ_CONV simplifies equations of the form t1 = t2,
where t1 and t2 are of type bool. When applied to a term of the form
t = t, the conversion bool_EQ_CONV returns the theorem
|- (t = t) = T
When applied to a term of the form t = T, the conversion returns
|- (t = T) = t
And when applied to a term of the form T = t, it returns
|- (T = t) = t
FAILURE
Fails unless applied to a term of the form t1 = t2, where t1 and t2 are
boolean, and either t1 and t2 are syntactically identical terms or one of
t1 and t2 is the constant T.
EXAMPLE
- bool_EQ_CONV (Parse.Term `T = F`);
val it = |- (T = F) = F : thm
- bool_EQ_CONV (Parse.Term `(0 < n) = T`);
val it = |- (0 < n = T) = 0 < n : thm