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 MHonArc.