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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and