equal
deleted
inserted
replaced
15 where |
15 where |
16 "bi (BP x t) = {x}" |
16 "bi (BP x t) = {x}" |
17 |
17 |
18 typ lam_raw |
18 typ lam_raw |
19 term VAR_raw |
19 term VAR_raw |
|
20 term APP_raw |
|
21 term LET_raw |
20 term Test.BP_raw |
22 term Test.BP_raw |
21 thm bi_raw.simps |
23 thm bi_raw.simps |
22 |
24 |
23 print_theorems |
25 print_theorems |
24 |
26 |
170 |
172 |
171 (* example 8 from Terms.thy *) |
173 (* example 8 from Terms.thy *) |
172 |
174 |
173 nominal_datatype foo8 = |
175 nominal_datatype foo8 = |
174 Foo0 "name" |
176 Foo0 "name" |
175 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in foo |
177 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" |
176 and bar8 = |
178 and bar8 = |
177 Bar0 "name" |
179 Bar0 "name" |
178 | Bar1 "name" s::"name" b::"bar8" bind s in b |
180 | Bar1 "name" s::"name" b::"bar8" bind s in b |
179 binder |
181 binder |
180 bv8 |
182 bv8 |
283 abbreviation |
285 abbreviation |
284 "atoms A \<equiv> atom ` A" |
286 "atoms A \<equiv> atom ` A" |
285 |
287 |
286 nominal_datatype trm = |
288 nominal_datatype trm = |
287 Var var |
289 Var var |
288 | LAM tv::tvar kind t::trm bind v in t |
290 | LAM tv::tvar kind t::trm bind tv in t |
289 | APP trm ty |
291 | APP trm ty |
290 | Lam v::var ty t::trm bind v in t |
292 | Lam v::var ty t::trm bind v in t |
291 | App trm trm |
293 | App trm trm |
292 | Let x::var ty trm t::trm bind x in t |
294 | Let x::var ty trm t::trm bind x in t |
293 | Case trm "assoc list" |
295 | Case trm "assoc list" |