Email Gateway (Aug 18 2022 at 11:08): Email Gateway (Aug 18 2022 at 11:08):From: Alberto Momigliano <amomigl1@inf.ed.ac.uk>
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,
A.
http://homepages.inf.ed.ac.uk/amomigl1/
Email Gateway (Aug 18 2022 at 11:08):From: Makarius <makarius@sketis.net>
The ancient isatool expandshort should do this for you -- it operates on
the original ML files, i.e. use it before isatool convert.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC