Re: [isabelle] naming facts



I suppose it might confuse some people. You can always call it kgt0 if you prefer. Random strings of letters strike me as being the worst option, because they convey no information whatever.

Larry Paulson


On 22 May 2012, at 11:50, John Wickerson wrote:

> Thanks Larry. Yes, I am aware of the chaining features (though not all of the features Johannes helpfully pointed out), and do try not to use my "random-name" trick *too* often. Regarding your suggestion of conflating variable-names and fact-names, I'm rather uneasy about this practice: doesn't it make the proof rather confusing if, for instance, "[OF k]" and "[of k]" are actually referring to different k's?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.