equal
deleted
inserted
replaced
901 lemma lets_ok: |
901 lemma lets_ok: |
902 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
902 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
903 apply (subst alpha5_INJ) |
903 apply (subst alpha5_INJ) |
904 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
904 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
905 apply (simp only: alpha_gen) |
905 apply (simp only: alpha_gen) |
906 apply (simp add: permute_trm5_lts) |
906 apply (simp add: permute_trm5_lts fresh_star_def) |
907 sorry |
907 apply (simp add: insert_eqvt eqvts atom_eqvt) |
908 |
908 done |
909 |
909 |
910 text {* type schemes *} |
910 text {* type schemes *} |
911 datatype ty = |
911 datatype ty = |
912 Var "name" |
912 Var "name" |
913 | Fun "ty" "ty" |
913 | Fun "ty" "ty" |