equal
deleted
inserted
replaced
8 |
8 |
9 thm finite_sets_supp |
9 thm finite_sets_supp |
10 |
10 |
11 nominal_datatype foo = |
11 nominal_datatype foo = |
12 Foo0 "name" |
12 Foo0 "name" |
13 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f |
13 | Foo1 b::"bar" f::"foo" binds (set) "bv b" in f |
14 and bar = |
14 and bar = |
15 Bar0 "name" |
15 Bar0 "name" |
16 | Bar1 "name" s::"name" b::"bar" bind (set) s in b |
16 | Bar1 "name" s::"name" b::"bar" binds (set) s in b |
17 binder |
17 binder |
18 bv |
18 bv |
19 where |
19 where |
20 "bv (Bar0 x) = {}" |
20 "bv (Bar0 x) = {}" |
21 | "bv (Bar1 v x b) = {atom v}" |
21 | "bv (Bar1 v x b) = {atom v}" |