equal
deleted
inserted
replaced
9 | APP "lam" "lam" |
9 | APP "lam" "lam" |
10 | LET bp::"bp" t::"lam" bind "bi bp" in t |
10 | LET bp::"bp" t::"lam" bind "bi bp" in t |
11 and bp = |
11 and bp = |
12 BP "name" "lam" |
12 BP "name" "lam" |
13 binder |
13 binder |
14 bi::"bp \<Rightarrow> name set" |
14 bi::"bp \<Rightarrow> atom set" |
15 where |
15 where |
16 "bi (BP x t) = {x}" |
16 "bi (BP x t) = {atom x}" |
17 |
17 |
18 typ lam_raw |
18 typ lam_raw |
19 term VAR_raw |
19 term VAR_raw |
20 term APP_raw |
20 term APP_raw |
21 term LET_raw |
21 term LET_raw |
22 term Test.BP_raw |
22 term Test.BP_raw |
23 thm bi_raw.simps |
23 thm bi_raw.simps |
|
24 thm permute_lam_raw_permute_bp_raw.simps |
|
25 thm alpha_lam_raw_alpha_bp_raw.intros |
24 |
26 |
25 print_theorems |
27 print_theorems |
26 |
28 |
27 text {* example 2 *} |
29 text {* example 2 *} |
28 |
30 |