| changeset 2634 | 3ce1089cdbf3 |
| parent 2622 | e6e6a3da81aa |
| child 2950 | 0911cb7bf696 |
| 2633:d1d09177ec89 | 2634:3ce1089cdbf3 |
|---|---|
30 text {* restricting a finite set of names *} |
30 text {* restricting a finite set of names *} |
31 |
31 |
32 nominal_datatype trm3 = |
32 nominal_datatype trm3 = |
33 Var3 "name" |
33 Var3 "name" |
34 | App3 "trm3" "trm3" |
34 | App3 "trm3" "trm3" |
35 | Lam3 xs::"name fset" t::"trm3" bind (res) xs in t |
35 | Lam3 xs::"name fset" t::"trm3" bind (set+) xs in t |
36 |
36 |
37 thm trm3.strong_exhaust |
37 thm trm3.eq_iff |
38 |
38 |
39 end |
39 end |
40 |
40 |
41 |
41 |
42 |
42 |