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