dropped theory PreList
authorhaftmann
Tue Apr 22 08:33:10 2008 +0200 (2008-04-22)
changeset 2672943a72d892594
parent 26728 1cfa52844c56
child 26730 bbb5e6904d78
dropped theory PreList
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList2/ToyList1
src/HOL/ATP_Linkup.thy
src/HOL/Main.thy
src/HOL/PreList.thy
     1.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Tue Apr 22 08:33:09 2008 +0200
     1.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Apr 22 08:33:10 2008 +0200
     1.3 @@ -1,12 +1,12 @@
     1.4  theory ToyList
     1.5 -imports PreList
     1.6 +imports Datatype
     1.7  begin
     1.8  
     1.9  text{*\noindent
    1.10 -HOL already has a predefined theory of lists called @{text"List"} ---
    1.11 -@{text"ToyList"} is merely a small fragment of it chosen as an example. In
    1.12 +HOL already has a predefined theory of lists called @{text List} ---
    1.13 +@{text ToyList} is merely a small fragment of it chosen as an example. In
    1.14  contrast to what is recommended in \S\ref{sec:Basic:Theories},
    1.15 -@{text"ToyList"} is not based on @{text"Main"} but on @{text"PreList"}, a
    1.16 +@{text ToyList} is not based on @{text Main} but on @{text Datatype}, a
    1.17  theory that contains pretty much everything but lists, thus avoiding
    1.18  ambiguities caused by defining lists twice.
    1.19  *}
     2.1 --- a/doc-src/TutorialI/ToyList2/ToyList1	Tue Apr 22 08:33:09 2008 +0200
     2.2 +++ b/doc-src/TutorialI/ToyList2/ToyList1	Tue Apr 22 08:33:10 2008 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  theory ToyList
     2.5 -imports PreList
     2.6 +imports Datatype
     2.7  begin
     2.8  
     2.9  datatype 'a list = Nil                          ("[]")
     3.1 --- a/src/HOL/ATP_Linkup.thy	Tue Apr 22 08:33:09 2008 +0200
     3.2 +++ b/src/HOL/ATP_Linkup.thy	Tue Apr 22 08:33:10 2008 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  header{* The Isabelle-ATP Linkup *}
     3.5  
     3.6  theory ATP_Linkup
     3.7 -imports PreList Hilbert_Choice
     3.8 +imports Record Presburger SAT Recdef Extraction Relation_Power Hilbert_Choice
     3.9     (*FIXME It must be a parent or a child of every other theory, to prevent theory-merge errors. FIXME*)
    3.10  uses
    3.11    "Tools/polyhash.ML"
     4.1 --- a/src/HOL/Main.thy	Tue Apr 22 08:33:09 2008 +0200
     4.2 +++ b/src/HOL/Main.thy	Tue Apr 22 08:33:10 2008 +0200
     4.3 @@ -8,11 +8,6 @@
     4.4  imports Map
     4.5  begin
     4.6  
     4.7 -text {*
     4.8 -  Theory @{text Main} includes everything.  Note that theory @{text
     4.9 -  PreList} already includes most HOL theories.
    4.10 -*}
    4.11 -
    4.12  ML {* val HOL_proofs = ! Proofterm.proofs *}
    4.13  
    4.14  ML {* path_add "~~/src/HOL/Library" *}
     5.1 --- a/src/HOL/PreList.thy	Tue Apr 22 08:33:09 2008 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,18 +0,0 @@
     5.4 -(*  Title:      HOL/PreList.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Nipkow and Markus Wenzel
     5.7 -    Copyright   2000 TU Muenchen
     5.8 -*)
     5.9 -
    5.10 -header {* A Basis for Building the Theory of Lists *}
    5.11 -
    5.12 -theory PreList
    5.13 -imports Record Presburger SAT Recdef Extraction Relation_Power
    5.14 -begin
    5.15 -
    5.16 -text {*
    5.17 -  This is defined separately to serve as a basis for
    5.18 -  theory ToyList in the documentation.
    5.19 -*}
    5.20 -
    5.21 -end