changeset 57243 | 8c261f0a9b32 |
parent 57231 | dca8d06ecbba |
child 57248 | 5496011859eb |
--- a/src/HOL/List.thy Thu Jun 12 17:02:03 2014 +0200 +++ b/src/HOL/List.thy Thu Jun 12 17:02:03 2014 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product +imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product begin datatype_new (set: 'a) list =