# HG changeset patch
# User wenzelm
# Date 1400954846 -7200
# Node ID 5c26000e1042520d71d4d3db61b3d5565d4cefac
# Parent  2c1c8b38e3f0c01fb2b0d0cdc91d869f4426e1ba
more portable file names;

diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/ROOT
--- a/src/Doc/ROOT	Sat May 24 19:15:04 2014 +0200
+++ b/src/Doc/ROOT	Sat May 24 20:07:26 2014 +0200
@@ -406,8 +406,8 @@
     "Sets/Relations"
     "Sets/Recur"
   document_files (in "ToyList")
-    "ToyList1"
-    "ToyList2"
+    "ToyList1.txt"
+    "ToyList2.txt"
   document_files (in "..")
     "pdfsetup.sty"
     "ttbox.sty"
diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/Tutorial/ToyList/ToyList1
--- a/src/Doc/Tutorial/ToyList/ToyList1	Sat May 24 19:15:04 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-theory ToyList
-imports Datatype
-begin
-
-datatype 'a list = Nil                          ("[]")
-                 | Cons 'a "'a list"            (infixr "#" 65)
-
-(* This is the append function: *)
-primrec app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
-where
-"[] @ ys       = ys" |
-"(x # xs) @ ys = x # (xs @ ys)"
-
-primrec rev :: "'a list => 'a list" where
-"rev []        = []" |
-"rev (x # xs)  = (rev xs) @ (x # [])"
diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/Tutorial/ToyList/ToyList1.txt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/ToyList/ToyList1.txt	Sat May 24 20:07:26 2014 +0200
@@ -0,0 +1,16 @@
+theory ToyList
+imports Datatype
+begin
+
+datatype 'a list = Nil                          ("[]")
+                 | Cons 'a "'a list"            (infixr "#" 65)
+
+(* This is the append function: *)
+primrec app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
+where
+"[] @ ys       = ys" |
+"(x # xs) @ ys = x # (xs @ ys)"
+
+primrec rev :: "'a list => 'a list" where
+"rev []        = []" |
+"rev (x # xs)  = (rev xs) @ (x # [])"
diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/Tutorial/ToyList/ToyList2
--- a/src/Doc/Tutorial/ToyList/ToyList2	Sat May 24 19:15:04 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-lemma app_Nil2 [simp]: "xs @ [] = xs"
-apply(induct_tac xs)
-apply(auto)
-done
-
-lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
-apply(induct_tac xs)
-apply(auto)
-done
-
-lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
-apply(induct_tac xs)
-apply(auto)
-done
-
-theorem rev_rev [simp]: "rev(rev xs) = xs"
-apply(induct_tac xs)
-apply(auto)
-done
-
-end
diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/Tutorial/ToyList/ToyList2.txt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/ToyList/ToyList2.txt	Sat May 24 20:07:26 2014 +0200
@@ -0,0 +1,21 @@
+lemma app_Nil2 [simp]: "xs @ [] = xs"
+apply(induct_tac xs)
+apply(auto)
+done
+
+lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
+apply(induct_tac xs)
+apply(auto)
+done
+
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
+apply(induct_tac xs)
+apply(auto)
+done
+
+theorem rev_rev [simp]: "rev(rev xs) = xs"
+apply(induct_tac xs)
+apply(auto)
+done
+
+end
diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/Tutorial/ToyList/ToyList_Test.thy
--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat May 24 19:15:04 2014 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat May 24 20:07:26 2014 +0200
@@ -6,7 +6,7 @@
   let
     val texts =
       map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
-        ["ToyList1", "ToyList2"];
+        ["ToyList1.txt", "ToyList2.txt"];
     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;
diff -r 2c1c8b38e3f0 -r 5c26000e1042 src/Doc/Tutorial/document/fp.tex
--- a/src/Doc/Tutorial/document/fp.tex	Sat May 24 19:15:04 2014 +0200
+++ b/src/Doc/Tutorial/document/fp.tex	Sat May 24 20:07:26 2014 +0200
@@ -26,7 +26,7 @@
 
 \begin{figure}[htbp]
 \begin{ttbox}\makeatother
-\input{ToyList1}\end{ttbox}
+\input{ToyList1.txt}\end{ttbox}
 \caption{A Theory of Lists}
 \label{fig:ToyList}
 \end{figure}
@@ -44,7 +44,7 @@
 
 \begin{figure}[htbp]
 \begin{ttbox}\makeatother
-\input{ToyList2}\end{ttbox}
+\input{ToyList2.txt}\end{ttbox}
 \caption{Proofs about Lists}
 \label{fig:ToyList-proofs}
 \end{figure}