[isabelle] Naive question about tactics and Pure



Hi,

I have a rather naive question about the use of terminology. AFAIK,
tactics are implemented in the meta-level and the meta-level language
in Isabelle is Pure. So is it correct to say that "tactics are written
in Pure"?

Thanks

John





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