changeset 35827 | f552152d7747 |
parent 35608 | db4045d1406e |
child 35828 | 46cfc4b8112e |
--- a/src/HOL/List.thy Wed Mar 17 19:26:05 2010 +0100 +++ b/src/HOL/List.thy Wed Mar 17 19:37:44 2010 +0100 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Presburger ATP_Linkup Recdef +imports Plain Presburger Sledgehammer Recdef uses ("Tools/list_code.ML") begin