equal
deleted
inserted
replaced
26 term LET_raw |
26 term LET_raw |
27 term Test.BP_raw |
27 term Test.BP_raw |
28 thm bi_raw.simps |
28 thm bi_raw.simps |
29 thm permute_lam_raw_permute_bp_raw.simps |
29 thm permute_lam_raw_permute_bp_raw.simps |
30 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars] |
30 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars] |
31 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
31 (*thm fv_lam_raw_fv_bp_raw.simps[no_vars]*) |
32 |
32 |
33 text {* example 2 *} |
33 text {* example 2 *} |
34 |
34 |
35 nominal_datatype trm' = |
35 nominal_datatype trm' = |
36 Var "name" |
36 Var "name" |
55 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
55 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
56 *) |
56 *) |
57 |
57 |
58 |
58 |
59 thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars] |
59 thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars] |
60 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
60 (*thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]*) |
61 thm f_raw.simps |
61 thm f_raw.simps |
62 (*thm trm'_pat'_induct |
62 (*thm trm'_pat'_induct |
63 thm trm'_pat'_perm |
63 thm trm'_pat'_perm |
64 thm trm'_pat'_fv |
64 thm trm'_pat'_fv |
65 thm trm'_pat'_bn |
65 thm trm'_pat'_bn |
88 thm trm0_pat0_bn*) |
88 thm trm0_pat0_bn*) |
89 |
89 |
90 text {* example type schemes *} |
90 text {* example type schemes *} |
91 |
91 |
92 nominal_datatype t = |
92 nominal_datatype t = |
93 Var "name" |
93 VarTS "name" |
94 | Fun "t" "t" |
94 | FunTS "t" "t" |
95 and tyS = |
95 and tyS = |
96 All xs::"name set" ty::"t" bind xs in ty |
96 All xs::"name set" ty::"t" bind xs in ty |
97 |
97 |
98 (* example 1 from Terms.thy *) |
98 (* example 1 from Terms.thy *) |
99 |
99 |