[isabelle-dev] fconv_rule

Makarius makarius at sketis.net
Tue Jul 3 13:19:21 CEST 2007


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


	Makarius



More information about the isabelle-dev mailing list