Re: [isabelle] isatool convert



On Thu, 13 Dec 2007, Alberto Momigliano wrote:

> br allI 1 would be translated in apply(rule allI) and similarly for other
> abbreviations ba,be,bes etc... ?

The ancient isatool expandshort should do this for you -- it operates on 
the original ML files, i.e. use it before isatool convert.


	Makarius





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