[isabelle] isatool convert

Dear all,

while I find the new Isabelle 2007 features wonderful, I am a bit sad of seeing ML scripts go, especially since isatool convert could be improved. I'm afraid that my perl understanding is so limited that my attempts to increase its functionality have gone nowhere. Would it be possible to add instructions so that, for example:

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

Also it would be great if in the default case, i.e. when "convert" does not understand a tactic, say T, it could return something like apply(tactic {* T *}), with the appropriate thm annotations, or am I asking too much?

Thanks for the help and all the best,


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