equal
deleted
inserted
replaced
889 lemma lets_ok: |
889 lemma lets_ok: |
890 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
890 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
891 apply (subst alpha5_INJ) |
891 apply (subst alpha5_INJ) |
892 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
892 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
893 apply (simp only: alpha_gen) |
893 apply (simp only: alpha_gen) |
894 apply (simp add: permute_trm5_lts) |
894 apply (simp add: permute_trm5_lts fresh_star_def) |
895 sorry |
895 apply (simp add: insert_eqvt eqvts atom_eqvt) |
896 |
896 done |
897 |
897 |
898 text {* type schemes *} |
898 text {* type schemes *} |
899 datatype ty = |
899 datatype ty = |
900 Var "name" |
900 Var "name" |
901 | Fun "ty" "ty" |
901 | Fun "ty" "ty" |