equal
deleted
inserted
replaced
105 apply(simp) |
105 apply(simp) |
106 done |
106 done |
107 |
107 |
108 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
108 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
109 |
109 |
110 ML {* val _ = cheat_alpha_eqvt := true *} |
|
111 ML {* val _ = recursive := true *} |
110 ML {* val _ = recursive := true *} |
112 |
111 |
113 nominal_datatype lam' = |
112 nominal_datatype lam' = |
114 VAR' "name" |
113 VAR' "name" |
115 | APP' "lam'" "lam'" |
114 | APP' "lam'" "lam'" |