equal
deleted
inserted
replaced
18 |
18 |
19 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
19 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
20 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
20 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
21 *) |
21 *) |
22 |
22 |
23 (* example 8 from Terms.thy *) |
|
24 |
|
25 (* Binding in a term under a bn, needs to fail *) |
|
26 (* |
|
27 nominal_datatype foo8 = |
|
28 Foo0 "name" |
|
29 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" |
|
30 and bar8 = |
|
31 Bar0 "name" |
|
32 | Bar1 "name" s::"name" b::"bar8" bind s in b |
|
33 binder |
|
34 bv8 |
|
35 where |
|
36 "bv8 (Bar0 x) = {}" |
|
37 | "bv8 (Bar1 v x b) = {atom v}" |
|
38 *) |
|
39 |
|
40 end |
23 end |
41 |
24 |
42 |
25 |