--- a/src/Doc/ROOT Tue Sep 03 11:29:01 2013 +0200
+++ b/src/Doc/ROOT Tue Sep 03 11:55:59 2013 +0200
@@ -284,6 +284,8 @@
session Tutorial (doc) in "Tutorial" = HOL +
options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
+ theories [threads = 1]
+ "ToyList/ToyList_Test"
theories [thy_output_indent = 5]
"ToyList/ToyList"
"Ifexpr/Ifexpr"
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Tue Sep 03 11:29:01 2013 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Tue Sep 03 11:55:59 2013 +0200
@@ -2,18 +2,6 @@
imports Datatype
begin
-(*<*)
-ML {* (* FIXME somewhat non-standard, fragile *)
- let
- val texts =
- map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
- ["ToyList1", "ToyList2"];
- val trs = Outer_Syntax.parse Position.start (implode texts);
- val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
- in @{assert} (Toplevel.is_toplevel end_state) end;
-*}
-(*>*)
-
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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Tue Sep 03 11:55:59 2013 +0200
@@ -0,0 +1,16 @@
+theory ToyList_Test
+imports Datatype
+begin
+
+ML {* (* FIXME somewhat non-standard, fragile *)
+ let
+ val texts =
+ map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
+ ["ToyList1", "ToyList2"];
+ val trs = Outer_Syntax.parse Position.start (implode texts);
+ val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
+ in @{assert} (Toplevel.is_toplevel end_state) end;
+*}
+
+end
+