equal
deleted
inserted
replaced
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype trm = |
8 Var "name" |
8 Var "name" |
9 | App "trm" "trm" |
9 | App "trm" "trm" |
10 | Lam x::"name" t::"trm" bind_set x in t |
10 | Lam x::"name" t::"trm" bind_set x in t |
11 | Let a::"assg" t1::"trm" t2::"trm" bind_set "bn a" in t1 t2 |
11 | Let a::"assg" t::"trm" bind_set "bn a" in t |
12 |
12 |
13 and assg = |
13 and assg = |
14 As "name" "trm" |
14 As "name" "trm" |
15 binder |
15 binder |
16 bn::"assg \<Rightarrow> atom set" |
16 bn::"assg \<Rightarrow> atom set" |