| changeset 32318 | bca7fd849829 |
| parent 32317 | b4b871808223 |
| child 32351 | 96f9e6402403 |
| 32317:b4b871808223 | 32318:bca7fd849829 |
|---|---|
1 theory Predicate_Compile_ex |
1 theory Predicate_Compile_ex |
2 imports Complex_Main Predicate_Compile |
2 imports Main Predicate_Compile |
3 begin |
3 begin |
4 |
4 |
5 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where |
5 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where |
6 "even 0" |
6 "even 0" |
7 | "even n \<Longrightarrow> odd (Suc n)" |
7 | "even n \<Longrightarrow> odd (Suc n)" |