equal
deleted
inserted
replaced
1 (* ID: $Id$ *) |
1 (* ID: $Id$ *) |
2 theory Even imports Main begin |
2 theory Even imports Main begin |
3 |
3 |
4 |
4 |
5 consts even :: "nat set" |
5 inductive_set even :: "nat set" |
6 inductive even |
6 where |
7 intros |
7 zero[intro!]: "0 \<in> even" |
8 zero[intro!]: "0 \<in> even" |
8 | step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even" |
9 step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even" |
|
10 |
9 |
11 text{*An inductive definition consists of introduction rules. |
10 text{*An inductive definition consists of introduction rules. |
12 |
11 |
13 @{thm[display] even.step[no_vars]} |
12 @{thm[display] even.step[no_vars]} |
14 \rulename{even.step} |
13 \rulename{even.step} |