# HG changeset patch
# User haftmann
# Date 1288103961 -7200
# Node ID 430fff4a91679e987fff7f7195e1b6abc7066448
# Parent  a402043d267a04383fa8dfe905b5fa634538f4e2
include ATP in theory List -- avoid theory edge by-passing the prominent list theory

diff -r a402043d267a -r 430fff4a9167 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 26 15:06:36 2010 +0200
+++ b/src/HOL/List.thy	Tue Oct 26 16:39:21 2010 +0200
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Plain Presburger Recdef Code_Numeral Quotient
+imports Plain Presburger Recdef Code_Numeral Quotient ATP
 uses ("Tools/list_code.ML")
 begin