changeset 37465 | fcc2c36b3770 |
parent 37456 | 0a1cc2675958 |
parent 37457 | 7201c7e0db87 |
child 37605 | 625bc011768a |
--- a/src/HOL/List.thy Fri Jun 18 20:22:06 2010 +0200 +++ b/src/HOL/List.thy Fri Jun 18 21:22:05 2010 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Plain Presburger Sledgehammer Recdef +imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef uses ("Tools/list_code.ML") begin