[isabelle] Turnstile



Dear list,

Is there an equivalent to turnstile in Isabelle?  In good old
mathematics and in other HOL systems, the turnstile (|-) has two roles:
to indicate that a theorem has been proved, and to separate any
assumptions of the theorem from its conclusion.

In Isabelle2005, if you return a theorem in the read-eval-print-loop,
then if it has one assumption 'P' and conclusion 'Q' then it gets
printed as "Q [P]" (if the flag for showing hypotheses is set), but just
as "Q" if there are no assumptions, and so this corresponds to the
second role.

But what about in more recent Isabelles?  I know that there's no
read-eval-print-loop as such, and that in Isar scripts you write
"theorem" before a formula, which is a bit like the first role but not
quite because until the proof is complete it states the intention that
the formula will be proved rather than that it has been proved.  Are
there ways of displaying lists of theorems, and if so how are these
presented?  I note that the printer for "Q [P]" is still there in the
Isabelle Pure source.  If anyone could shed any light on all of this
then I'd be most grateful.

Mark.


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