Re: [isabelle] I need a meta-or
On Wed, 31 Jul 2013, Gottfried Barrow wrote:
It's a syntax priority problem.
Trueprop priority is 5, so dealing with the syntax of functions of type "prop
=> prop" and "prop => prop => prop" is tricky:
Trueprop :: "bool => prop" ("(_)" 5)
If you want to play with syntax, you can always use 'notation' and
'no_notation' to specify things in any way you like, but don't ask me
about suitable priorities -- this is a black art and better not changed
Generally, Isabelle/Pure is not really a meta-logic, i.e. a logic to
reason about other logics. It is just a logical framework, for
higher-order natural deduction based on !! and ==>.
If you really want to reason about some other logic, better do it in
Isabelle/HOL, and define you syntax as datatype, semantics as function,
inference system as inductive predicate in the usual way. AFP has
examples for that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and