# 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
``meta operators
`

`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
proof -
show A sorry
show B sorry
show C sorry
qed

`You better chose to ignore that the internal system state somewhere
``involves "A &&& B &&& C" -- it is never encountered in a regular proof.
`
Makarius

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