[isabelle] Isar tutorial example broken?



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
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





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