Hi,
Assuming you meant the right (assume, and show + proof).
You can not prove "A" even after assuming "A", when you don't use it.
so something like
assume "A" show "A"
is the same as
show "A" (which is a little bit difficult to prove).
Indeed
assume "A"
show "A" .
used to work, where Isabelle/Isar used to figure out that you meant to
use an assumption. This "feature" was judged later to be "bug" and that
for readable natural deduction proofs, one needs to specify all the
assmptions one uses. (For a year or so, the system used to output a
legacy feature message I think).
Amine.

`
``
`Chris Capel wrote:

I'm working through the isar tutorial by Tobias Nipkow, and didn't get
very far before finding a problem.
lemma "A --> A"
assume "A"
shows "A" .
qed
This example fails at the proof of shows, with an empty result
sequence. I am using the repository version of isabelle with the HOL
theory loaded, and my theory imports Main and doesn't do anything
else. I'm using ProofGeneral. The preceding example, where the
assumption is named and referenced with "by (rule a)" works. Is this
something broken in the repository?
Chris Capel

`
`