Next: , Previous: , Up: Isabelle/Isar   [Contents]


10.1.3 lemma and theorem keywords

Lemmas and theorems are treated the same. Lemmas end up as the goals of the proofs that Aris creates, and are the actual sentences that can be deduced. It takes the ’if-then’ form of each lemma.