equal
deleted
inserted
replaced
146 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
146 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
147 (*thm lam_bp_induct |
147 (*thm lam_bp_induct |
148 thm lam_bp_perm |
148 thm lam_bp_perm |
149 thm lam_bp_fv |
149 thm lam_bp_fv |
150 thm lam_bp_bn |
150 thm lam_bp_bn |
151 thm lam_bp_inject*) |
151 thm lam_bp_inject |
|
152 thm lam_bp_distinct*) |
152 |
153 |
153 text {* example 2 *} |
154 text {* example 2 *} |
154 |
155 |
155 nominal_datatype trm' = |
156 nominal_datatype trm' = |
156 Var "name" |
157 Var "name" |