equal
deleted
inserted
replaced
649 qed "mgu_new"; |
649 qed "mgu_new"; |
650 |
650 |
651 |
651 |
652 (* lemmata for substitutions *) |
652 (* lemmata for substitutions *) |
653 |
653 |
654 goalw Type.thy [app_subst_list] "length ($ S A) = length A"; |
654 goalw Type.thy [app_subst_list] |
|
655 "!!A:: ('a::type_struct) list. length ($ S A) = length A"; |
655 by (Simp_tac 1); |
656 by (Simp_tac 1); |
656 qed "length_app_subst_list"; |
657 qed "length_app_subst_list"; |
657 Addsimps [length_app_subst_list]; |
658 Addsimps [length_app_subst_list]; |
658 |
659 |
659 goal thy "!!sch::type_scheme. $ TVar sch = sch"; |
660 goal thy "!!sch::type_scheme. $ TVar sch = sch"; |