equal
deleted
inserted
replaced
200 BP "name" "lam" ("_ ::= _" [100,100] 100) |
200 BP "name" "lam" ("_ ::= _" [100,100] 100) |
201 binder |
201 binder |
202 bi::"bp \<Rightarrow> name set" |
202 bi::"bp \<Rightarrow> name set" |
203 where |
203 where |
204 "bi (BP x t) = {x}" |
204 "bi (BP x t) = {x}" |
205 |
205 print_theorems |
206 |
206 |
207 text {* examples 2 *} |
207 text {* examples 2 *} |
208 nominal_datatype trm = |
208 nominal_datatype trm = |
209 Var "string" |
209 Var "name" |
210 | App "trm" "trm" |
210 | App "trm" "trm" |
211 | Lam x::"name" t::"trm" bindset x in t |
211 | Lam x::"name" t::"trm" bindset x in t |
212 | Let p::"pat" "trm" t::"trm" bind "f p" in t |
212 | Let p::"pat" "trm" t::"trm" bind "f p" in t |
213 and pat = |
213 and pat = |
214 PN |
214 PN |