# HG changeset patch
# User haftmann
# Date 1208845990 -7200
# Node ID 43a72d89259479453ea4d623fae84583ec286ef2
# Parent  1cfa52844c566a1e5ddde514ddb05dd024c172bf
dropped theory PreList

diff -r 1cfa52844c56 -r 43a72d892594 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Tue Apr 22 08:33:09 2008 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Apr 22 08:33:10 2008 +0200
@@ -1,12 +1,12 @@
 theory ToyList
-imports PreList
+imports Datatype
 begin
 
 text{*\noindent
-HOL already has a predefined theory of lists called @{text"List"} ---
-@{text"ToyList"} is merely a small fragment of it chosen as an example. In
+HOL already has a predefined theory of lists called @{text List} ---
+@{text ToyList} is merely a small fragment of it chosen as an example. In
 contrast to what is recommended in \S\ref{sec:Basic:Theories},
-@{text"ToyList"} is not based on @{text"Main"} but on @{text"PreList"}, a
+@{text ToyList} is not based on @{text Main} but on @{text Datatype}, a
 theory that contains pretty much everything but lists, thus avoiding
 ambiguities caused by defining lists twice.
 *}
diff -r 1cfa52844c56 -r 43a72d892594 doc-src/TutorialI/ToyList2/ToyList1
--- a/doc-src/TutorialI/ToyList2/ToyList1	Tue Apr 22 08:33:09 2008 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1	Tue Apr 22 08:33:10 2008 +0200
@@ -1,5 +1,5 @@
 theory ToyList
-imports PreList
+imports Datatype
 begin
 
 datatype 'a list = Nil                          ("[]")
diff -r 1cfa52844c56 -r 43a72d892594 src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Tue Apr 22 08:33:09 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy	Tue Apr 22 08:33:10 2008 +0200
@@ -7,7 +7,7 @@
 header{* The Isabelle-ATP Linkup *}
 
 theory ATP_Linkup
-imports PreList Hilbert_Choice
+imports Record Presburger SAT Recdef Extraction Relation_Power Hilbert_Choice
    (*FIXME It must be a parent or a child of every other theory, to prevent theory-merge errors. FIXME*)
 uses
   "Tools/polyhash.ML"
diff -r 1cfa52844c56 -r 43a72d892594 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Apr 22 08:33:09 2008 +0200
+++ b/src/HOL/Main.thy	Tue Apr 22 08:33:10 2008 +0200
@@ -8,11 +8,6 @@
 imports Map
 begin
 
-text {*
-  Theory @{text Main} includes everything.  Note that theory @{text
-  PreList} already includes most HOL theories.
-*}
-
 ML {* val HOL_proofs = ! Proofterm.proofs *}
 
 ML {* path_add "~~/src/HOL/Library" *}
diff -r 1cfa52844c56 -r 43a72d892594 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Tue Apr 22 08:33:09 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/PreList.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel
-    Copyright   2000 TU Muenchen
-*)
-
-header {* A Basis for Building the Theory of Lists *}
-
-theory PreList
-imports Record Presburger SAT Recdef Extraction Relation_Power
-begin
-
-text {*
-  This is defined separately to serve as a basis for
-  theory ToyList in the documentation.
-*}
-
-end