| changeset 1313 | da44ef9a7df2 |
| parent 1312 | b0eae8c93314 |
| parent 1309 | b395b902cf0d |
| child 1317 | a8627c3bdd0c |
| child 1319 | d793ce9cd06f |
| 1312:b0eae8c93314 | 1313:da44ef9a7df2 |
|---|---|
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 |