# HG changeset patch
# User wenzelm
# Date 1415373185 -3600
# Node ID baf5a3c28f0cfe5c3652406e7c426abad7359174
# Parent  1b655309617c6e02b9fe64e88fdb39450e8c0c68
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;

diff -r 1b655309617c -r baf5a3c28f0c src/Doc/Tutorial/ToyList/ToyList.thy
--- a/src/Doc/Tutorial/ToyList/ToyList.thy	Fri Nov 07 15:19:30 2014 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Fri Nov 07 16:13:05 2014 +0100
@@ -1,16 +1,18 @@
 theory ToyList
-imports BNF_Least_Fixpoint
+imports Main
 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
-contrast to what is recommended in \S\ref{sec:Basic:Theories},
-@{text ToyList} is not based on @{text Main} but on
-@{text BNF_Least_Fixpoint}, a theory that contains pretty much everything
-but lists, thus avoiding ambiguities caused by defining lists twice.
+@{text ToyList} is merely a small fragment of it chosen as an example.
+To avoid some ambiguities caused by defining lists twice, we manipulate
+the concrete syntax and name space of theory @{theory Main} as follows.
 *}
 
+no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
+hide_type list
+hide_const rev
+
 datatype 'a list = Nil                          ("[]")
                  | Cons 'a "'a list"            (infixr "#" 65)
 
diff -r 1b655309617c -r baf5a3c28f0c src/Doc/Tutorial/ToyList/ToyList1.txt
--- a/src/Doc/Tutorial/ToyList/ToyList1.txt	Fri Nov 07 15:19:30 2014 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList1.txt	Fri Nov 07 16:13:05 2014 +0100
@@ -1,7 +1,11 @@
 theory ToyList
-imports BNF_Least_Fixpoint
+imports Main
 begin
 
+no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
+hide_type list
+hide_const rev
+
 datatype 'a list = Nil                          ("[]")
                  | Cons 'a "'a list"            (infixr "#" 65)
 
diff -r 1b655309617c -r baf5a3c28f0c src/Doc/Tutorial/ToyList/ToyList_Test.thy
--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Fri Nov 07 15:19:30 2014 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Fri Nov 07 16:13:05 2014 +0100
@@ -1,5 +1,5 @@
 theory ToyList_Test
-imports BNF_Least_Fixpoint
+imports Main
 begin
 
 ML {*
@@ -7,7 +7,7 @@
     map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
       ["ToyList1.txt", "ToyList2.txt"]
     |> implode
-  in Thy_Info.script_thy Position.start text @{theory BNF_Least_Fixpoint} end
+  in Thy_Info.script_thy Position.start text @{theory} end
 *}
 
 end