Re: [isabelle] antiquotations

Makarius wrote:

So, is there some reason this is not possible? In particular, Isar is executed in ML, so it seems rather strange to me that you cannot replicate it's effect in ML, for example by pasting the function calls used by Isar into the ML.

Since the Isar toplevel is more powerful than the raw ML one,
I don't get this. Is it in fact true that Isabelle (including Isar) is (entirely) written in ML?
If so, how can you do things in Isar that can't be done in ML?



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