changeset 6153 | bff90585cce5 |
parent 6141 | a6922171b396 |
child 9491 | 1a36151ee2fc |
--- a/src/ZF/List.ML Mon Jan 25 20:35:19 1999 +0100 +++ b/src/ZF/List.ML Wed Jan 27 10:31:31 1999 +0100 @@ -166,9 +166,7 @@ [list_rec_type, map_type, map_type2, app_type, length_type, rev_type, flat_type, list_add_type]; -Addsimps list_typechecks; - -simpset_ref() := simpset() setSolver (type_auto_tac list_typechecks); +AddTCs list_typechecks; (*** theorems about map ***)