169 qed "postorder_type"; |
169 qed "postorder_type"; |
170 |
170 |
171 |
171 |
172 (** Term simplification **) |
172 (** Term simplification **) |
173 |
173 |
174 val term_typechecks = |
174 AddTCs [term.Apply_I, term_map_type, term_map_type2, term_size_type, |
175 [term.Apply_I, term_map_type, term_map_type2, term_size_type, |
175 reflect_type, preorder_type, postorder_type]; |
176 reflect_type, preorder_type, postorder_type]; |
|
177 |
176 |
178 (*map_type2 and term_map_type2 instantiate variables*) |
177 (*map_type2 and term_map_type2 instantiate variables*) |
179 simpset_ref() := simpset() |
178 Addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]; |
180 addsimps [term_rec, term_map, term_size, reflect, preorder, postorder] |
|
181 setSolver type_auto_tac (list_typechecks@term_typechecks); |
|
182 |
179 |
183 |
180 |
184 (** theorems about term_map **) |
181 (** theorems about term_map **) |
185 |
182 |
186 Addsimps [thm "List.map_compose"]; (*there is also TF.map_compose*) |
183 Addsimps [thm "List.map_compose"]; (*there is also TF.map_compose*) |