equal
deleted
inserted
replaced
189 apply(simp) |
189 apply(simp) |
190 done |
190 done |
191 |
191 |
192 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
192 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
193 |
193 |
194 ML {* val _ = cheat_alpha_eqvt := true *} |
|
195 ML {* val _ = recursive := true *} |
194 ML {* val _ = recursive := true *} |
196 |
195 |
197 nominal_datatype lam' = |
196 nominal_datatype lam' = |
198 VAR' "name" |
197 VAR' "name" |
199 | APP' "lam'" "lam'" |
198 | APP' "lam'" "lam'" |