Re: [isabelle] Naive question about tactics and Pure
I think there is one more level: the ML level. You can do things on the
ML level that you cannot do inside Pure or any object logic. Tactics are
implemented on the ML level. Maybe there is no clear-cut border between
Pure and the ML level. But I rather think about the former as a formal
logic and the latter as a programming language (which it is).
To be a bit more precise (I hope). Everything origins from the ML level,
since it is implemented in the programming language ML, but the part
which I would call Pure (concerned with the implementation of a minimal
higher-order logic that serves as logical framework for arbitrary object
logics) is not whole of ML, but just some specific types and functions
that serve as an interface.
Hence when you do anything in Pure it corresponds to some function call
in ML and when you call ML functions from the specific interface it
corresponds to some manipulation of Pure terms (which might or might not
be expressible in the logic itself). But there is definitely a large
space of ML functions that is not related to Pure.
Hope this makes any sense.
On 08/28/2012 08:04 AM, John Munroe wrote:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and