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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and