changeset 51112 | da97167e03f7 |
parent 51096 | 60e4b75fefe1 |
child 51160 | 599ff65b85e2 |
--- a/src/HOL/List.thy Thu Feb 14 13:16:47 2013 +0100 +++ b/src/HOL/List.thy Thu Feb 14 12:24:42 2013 +0100 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Presburger Code_Numeral Quotient ATP +imports Presburger Code_Numeral Quotient ATP begin datatype 'a list =