equal
deleted
inserted
replaced
205 |
205 |
206 Below we give two definitions for the transitive closure |
206 Below we give two definitions for the transitive closure |
207 *} |
207 *} |
208 |
208 |
209 inductive |
209 inductive |
210 eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) |
210 eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 60) |
211 where |
211 where |
212 e_Lam[intro]: "Lam [x].t \<Down> Lam [x].t" |
212 e_Lam[intro]: "Lam [x].t \<Down> Lam [x].t" |
213 | e_App[intro]: "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v" |
213 | e_App[intro]: "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v" |
214 |
214 |
215 text {* |
215 text {* |