equal
deleted
inserted
replaced
131 |
131 |
132 lemma o_id_subst [simp]: "$s o id_subst = s" |
132 lemma o_id_subst [simp]: "$s o id_subst = s" |
133 by (rule ext) (simp add: id_subst_def) |
133 by (rule ext) (simp add: id_subst_def) |
134 |
134 |
135 lemma dom_id_subst [simp]: "dom id_subst = {}" |
135 lemma dom_id_subst [simp]: "dom id_subst = {}" |
136 by (simp add: dom_def id_subst_def empty_def) |
136 by (simp add: dom_def id_subst_def) |
137 |
137 |
138 lemma cod_id_subst [simp]: "cod id_subst = {}" |
138 lemma cod_id_subst [simp]: "cod id_subst = {}" |
139 by (simp add: cod_def) |
139 by (simp add: cod_def) |
140 |
140 |
141 lemma free_tv_id_subst [simp]: "free_tv id_subst = {}" |
141 lemma free_tv_id_subst [simp]: "free_tv id_subst = {}" |