[isabelle-dev] fconv_rule

[Lawrence Paulson]

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.)