Re: [isabelle] How do I write the sequent |- P in Isar using theorem
On 7/1/2013 10:15 PM, Gottfried Barrow wrote:
At least to myself, I can now say things like, "Please consider |-
"[|A;B|] ==> A & B", <i(conjI,a,a>..."
And saying things like that are best only said to one's self. Moving
sets of assumptions back and forth from the LHS and RHS of the
turnstile would indicate a fundamental misunderstanding of basic logic,
of which the remembering of former textbook quotes can sometimes help
correct. It might be better to modify the notation and say something like:
Please consider |- <i(conjI),a,a> => "[|A;B|] ==> A & B"...
But that's the basic idea. Trying to tie into standard notation without
abusing it any more than necessary. If it's still messed up, I should be
eventually figure out how to make it acceptable.
This archive was generated by a fusion of
Pipermail (Mailman edition) and