equal
deleted
inserted
replaced
11 text {* binding lists of names *} |
11 text {* binding lists of names *} |
12 |
12 |
13 nominal_datatype trm1 = |
13 nominal_datatype trm1 = |
14 Var1 "name" |
14 Var1 "name" |
15 | App1 "trm1" "trm1" |
15 | App1 "trm1" "trm1" |
16 | Lam1 xs::"name list" t::"trm1" bind xs in t |
16 | Lam1 xs::"name list" t::"trm1" binds xs in t |
17 |
17 |
18 thm trm1.strong_exhaust |
18 thm trm1.strong_exhaust |
19 |
19 |
20 |
20 |
21 text {* binding a finite set of names *} |
21 text {* binding a finite set of names *} |
22 |
22 |
23 nominal_datatype trm2 = |
23 nominal_datatype trm2 = |
24 Var2 "name" |
24 Var2 "name" |
25 | App2 "trm2" "trm2" |
25 | App2 "trm2" "trm2" |
26 | Lam2 xs::"name fset" t::"trm2" bind (set) xs in t |
26 | Lam2 xs::"name fset" t::"trm2" binds (set) xs in t |
27 |
27 |
28 thm trm2.strong_exhaust |
28 thm trm2.strong_exhaust |
29 |
29 |
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 (set+) xs in t |
35 | Lam3 xs::"name fset" t::"trm3" binds (set+) xs in t |
36 |
36 |
37 thm trm3.eq_iff |
37 thm trm3.eq_iff |
38 |
38 |
39 end |
39 end |
40 |
40 |