It was called that in Cambridge LCF in 1983.
%Forward proof rule for conversions:
A
--------- where fconv A is A <=> B
B
%
let FCONV_RULE fconv =
set_fail_prefix `FCONV_RULE`
(\th. MP (CONJUNCT1 (IFF_CONJ (fconv (concl th)))) th);;
Larry
On 3 Jul 2007, at 11:14, Makarius wrote:
> Does anyboy remember why fconv_rule is called like this? After peeking
> into the HOL Light sources I've got the impression that this
> function is
> usually called conv_rule. (Conversions have become popular
> recently so it
> might be a good point to sort this out now.)
