[isabelle] trivial Isar proof fails



Hi,

on the bottom of page 3 of

http://arachne.it.uu.se/grad/courses/gc0910/isabelle/isar-overview.pdf#page=3

there is a proof

lemma "A ⟶ A"
proof
  assume "A"
  show "A" .

introducing dot as a trivial proof. In my 2013-2 installation it does not work:

Failed to finish proof:
goal (1 subgoal):
 1. A

What is the problem here?

- Gergely




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