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