# Re: [isabelle] Wanting only ==>, prop, and schematic variables; but not so

`It's not exactly all there, but starting on page 27 of isar-ref.pdf,
``there is section "2.1 The Pure Framework", in which a brief explanation
``of the four meta-logic symbols is given, where the four symbols are =>,
``\<And>, \<equiv>, and ==>. It pays to look at things 4 or 5 times, at least.
`

`In particular, on page 28, it says, "Logical statements are composed via
``\<And>x::alpha. B(x) and A ==> B." It then goes on to define some rules
``for \<And> and ==> using sequents.
`

`That's important because there is the section "Simulating sequents by
``natural deduction" on page 203 which talks about expressing a form of
``sequents using the ==> symbol.
`

`You put those sections together, and you might be able to figure how to
``use ==> to have a form of sequents in Isabelle/HOL where ==> is
``considered the fundamental symbol for the sequents, and figure out how
``to do it without abusing conventional standards too much.
`

`You might call them isa-sequents. If you abuse things unintentionally,
``an isa-sequent is whatever you define it be anyway.
`
Regards,
GB

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