equal
deleted
inserted
replaced
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := true *} |
7 ML {* val _ = recursive := true *} |
8 ML {* val _ = alpha_type := AlphaGen *} |
8 ML {* val _ = alpha_type := AlphaGen *} |
9 nominal_datatype lam' = |
9 nominal_datatype lam = |
10 VAR' "name" |
10 VAR "name" |
11 | APP' "lam'" "lam'" |
11 | APP "lam" "lam" |
12 | LAM' x::"name" t::"lam'" bind x in t |
12 | LAM x::"name" t::"lam" bind x in t |
13 | LET' bp::"bp'" t::"lam'" bind "bi' bp" in t |
13 | LET bp::"bp" t::"lam" bind "bi bp" in t |
14 and bp' = |
14 and bp = |
15 BP' "name" "lam'" |
15 BP "name" "lam" |
16 binder |
16 binder |
17 bi'::"bp' \<Rightarrow> atom set" |
17 bi::"bp \<Rightarrow> atom set" |
18 where |
18 where |
19 "bi' (BP' x t) = {atom x}" |
19 "bi (BP x t) = {atom x}" |
20 |
20 |
21 thm lam'_bp'.fv |
21 thm lam_bp.fv |
22 thm lam'_bp'.eq_iff[no_vars] |
22 thm lam_bp.eq_iff[no_vars] |
23 thm lam'_bp'.bn |
23 thm lam_bp.bn |
24 thm lam'_bp'.perm |
24 thm lam_bp.perm |
25 thm lam'_bp'.induct |
25 thm lam_bp.induct |
26 thm lam'_bp'.inducts |
26 thm lam_bp.inducts |
27 thm lam'_bp'.distinct |
27 thm lam_bp.distinct |
28 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
28 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
29 thm lam'_bp'.fv[simplified lam'_bp'.supp] |
29 thm lam_bp.fv[simplified lam_bp.supp] |
30 |
30 |
31 end |
31 end |
32 |
32 |
33 |
33 |
34 |
34 |