equal
deleted
inserted
replaced
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 |
24 thm permute_lam_raw_permute_bp_raw.simps |
25 thm alpha_lam_raw_alpha_bp_raw.intros |
25 thm alpha_lam_raw_alpha_bp_raw.intros |
26 thm fv_lam_raw_fv_bp_raw.simps |
26 thm fv_lam_raw_fv_bp_raw.simps |
27 |
27 thm eqvts |
28 |
28 |
29 print_theorems |
29 print_theorems |
30 |
30 |
31 text {* example 2 *} |
31 text {* example 2 *} |
32 |
32 |
330 bv :: "pat \<Rightarrow> atom set" |
330 bv :: "pat \<Rightarrow> atom set" |
331 where |
331 where |
332 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
332 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
333 *) |
333 *) |
334 |
334 |
335 thm bv_raw.simps |
|
336 |
|
337 end |
335 end |
338 |
336 |
339 |
337 |
340 |
338 |