| changeset 57231 | dca8d06ecbba |
| parent 57206 | d9be905d6283 |
| child 57243 | 8c261f0a9b32 |
| child 57247 | 8191ccf6a1bd |
--- a/src/HOL/List.thy Thu Jun 12 01:00:49 2014 +0200 +++ b/src/HOL/List.thy Thu Jun 12 01:00:49 2014 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product +imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product begin datatype_new (set: 'a) list =