Example. Rule Induction, Automation, Structured Proofs › Even numbers as an inductive [isa-002K]

inductive even :: "nat ⇒ bool" where even0: "even 0" | evenSS: "even n ⟹ even (Suc (Suc n))"