# 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.
`
Regards,
GB

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