equal
deleted
inserted
replaced
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" bind xs in t |
17 |
17 |
|
18 thm trm1.strong_exhaust |
|
19 |
18 |
20 |
19 text {* binding a finite set of names *} |
21 text {* binding a finite set of names *} |
20 |
22 |
21 nominal_datatype trm2 = |
23 nominal_datatype trm2 = |
22 Var2 "name" |
24 Var2 "name" |
23 | App2 "trm2" "trm2" |
25 | App2 "trm2" "trm2" |
24 | Lam2 xs::"name fset" t::"trm2" bind (set) xs in t |
26 | Lam2 xs::"name fset" t::"trm2" bind (set) xs in t |
25 |
27 |
|
28 thm trm2.strong_exhaust |
26 |
29 |
27 text {* restricting a finite set of names *} |
30 text {* restricting a finite set of names *} |
28 |
31 |
29 nominal_datatype trm3 = |
32 nominal_datatype trm3 = |
30 Var3 "name" |
33 Var3 "name" |
31 | App3 "trm3" "trm3" |
34 | App3 "trm3" "trm3" |
32 | Lam3 xs::"name fset" t::"trm3" bind (res) xs in t |
35 | Lam3 xs::"name fset" t::"trm3" bind (res) xs in t |
33 |
36 |
|
37 thm trm3.strong_exhaust |
34 |
38 |
35 end |
39 end |
36 |
40 |
37 |
41 |
38 |
42 |