equal
deleted
inserted
replaced
15 |
15 |
16 nominal_datatype ty = |
16 nominal_datatype ty = |
17 Var "name" |
17 Var "name" |
18 | Fun "ty" "ty" (infixr "\<rightarrow>" 100) |
18 | Fun "ty" "ty" (infixr "\<rightarrow>" 100) |
19 and tys = |
19 and tys = |
20 All as::"name fset" ty::"ty" bind (set+) as in ty ("All _. _" [100, 100] 100) |
20 All as::"name fset" ty::"ty" binds (set+) as in ty ("All _. _" [100, 100] 100) |
21 |
21 |
22 |
22 |
23 text {* Some alpha-equivalences *} |
23 text {* Some alpha-equivalences *} |
24 |
24 |
25 lemma |
25 lemma |