Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
authorhaftmann
Tue, 26 Oct 2010 16:39:21 +0200
changeset 40195 430fff4a9167
parent 40194 a402043d267a
child 40196 123b6fe379f6
child 40201 0dcd03b05da4
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle