Re: [isabelle] antiquotations
I don't get this. Is it in fact true that Isabelle (including Isar) is
(entirely) written in ML?
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,
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