--- 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.
*}
--- 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 ("[]")
--- 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"
--- 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" *}
--- 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