equal
deleted
inserted
replaced
37 lemma test: |
37 lemma test: |
38 "finite (supp (t::trm)) \<and> finite (supp (a::assg))" |
38 "finite (supp (t::trm)) \<and> finite (supp (a::assg))" |
39 apply(rule single_let.induct) |
39 apply(rule single_let.induct) |
40 apply(rule supports_finite) |
40 apply(rule supports_finite) |
41 apply(rule single_let.supports) |
41 apply(rule single_let.supports) |
42 apply(simp only: finite_supp supp_Pair finite_Un) |
42 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
43 apply(rule supports_finite) |
43 apply(rule supports_finite) |
44 apply(rule single_let.supports) |
44 apply(rule single_let.supports) |
45 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
45 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
46 apply(rule supports_finite) |
46 apply(rule supports_finite) |
47 apply(rule single_let.supports) |
47 apply(rule single_let.supports) |