Re: [isabelle] rule_format and locales



On Thu, 3 Aug 2006, Peter Lammich wrote:

> Can I use something similiar to rule_format that works inside a locale, 
> or do I have to transform the lemmas "by hand" ?

The easiest way is to avoid rule_format altogether, which is a legacy 
feature anyway.  If you state your problems with !!/==> or 
fixes/assumes/shows in the first place, the outcome will be in canonical 
rule format as expected.  (Note that the induct method will do the right 
thing on !!/==> goals).


	Makarius





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