[isabelle] trivial Isar proof fails


on the bottom of page 3 of


there is a proof

lemma "A ⟶ A"
  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.