Re: [isabelle] I need a meta-or
On Thu, 25 Jul 2013, Gottfried Barrow wrote:
There's the meta-and, &&&, but I need a meta-or, so I don't have to define
two meta-or operators to keep from using PROP.
If there's a &&&, then it seems there should be the complete suite of basic
In principle you could define all the standard connectives of Isabelle/HOL
in Isabelle/Pure as well, but what is the point?
The purpose of Isabelle/Pure is to provide a framework for higher-order
natural deduction, with declarative rule structure indicated by the
connectives !! and ==> (i.e. Minimal Higher-order Logic). Anything beyond
that is not really pure.
Note that &&& is merely used internally as auxilary device -- it should
hardly ever occur in applications of Isabelle/Pure (or HOL). You just use
multiple propositions directly in Isar like this:
lemma A and B and C
show A sorry
show B sorry
show C sorry
You better chose to ignore that the internal system state somewhere
involves "A &&& B &&& C" -- it is never encountered in a regular proof.
This archive was generated by a fusion of
Pipermail (Mailman edition) and