more portable file names;
authorwenzelm
Sat May 24 20:07:26 2014 +0200 (2014-05-24)
changeset 570835c26000e1042
parent 57082 2c1c8b38e3f0
child 57084 70e288a4b32d
more portable file names;
src/Doc/ROOT
src/Doc/Tutorial/ToyList/ToyList1
src/Doc/Tutorial/ToyList/ToyList1.txt
src/Doc/Tutorial/ToyList/ToyList2
src/Doc/Tutorial/ToyList/ToyList2.txt
src/Doc/Tutorial/ToyList/ToyList_Test.thy
src/Doc/Tutorial/document/fp.tex
     1.1 --- a/src/Doc/ROOT	Sat May 24 19:15:04 2014 +0200
     1.2 +++ b/src/Doc/ROOT	Sat May 24 20:07:26 2014 +0200
     1.3 @@ -406,8 +406,8 @@
     1.4      "Sets/Relations"
     1.5      "Sets/Recur"
     1.6    document_files (in "ToyList")
     1.7 -    "ToyList1"
     1.8 -    "ToyList2"
     1.9 +    "ToyList1.txt"
    1.10 +    "ToyList2.txt"
    1.11    document_files (in "..")
    1.12      "pdfsetup.sty"
    1.13      "ttbox.sty"
     2.1 --- a/src/Doc/Tutorial/ToyList/ToyList1	Sat May 24 19:15:04 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,16 +0,0 @@
     2.4 -theory ToyList
     2.5 -imports Datatype
     2.6 -begin
     2.7 -
     2.8 -datatype 'a list = Nil                          ("[]")
     2.9 -                 | Cons 'a "'a list"            (infixr "#" 65)
    2.10 -
    2.11 -(* This is the append function: *)
    2.12 -primrec app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
    2.13 -where
    2.14 -"[] @ ys       = ys" |
    2.15 -"(x # xs) @ ys = x # (xs @ ys)"
    2.16 -
    2.17 -primrec rev :: "'a list => 'a list" where
    2.18 -"rev []        = []" |
    2.19 -"rev (x # xs)  = (rev xs) @ (x # [])"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Doc/Tutorial/ToyList/ToyList1.txt	Sat May 24 20:07:26 2014 +0200
     3.3 @@ -0,0 +1,16 @@
     3.4 +theory ToyList
     3.5 +imports Datatype
     3.6 +begin
     3.7 +
     3.8 +datatype 'a list = Nil                          ("[]")
     3.9 +                 | Cons 'a "'a list"            (infixr "#" 65)
    3.10 +
    3.11 +(* This is the append function: *)
    3.12 +primrec app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
    3.13 +where
    3.14 +"[] @ ys       = ys" |
    3.15 +"(x # xs) @ ys = x # (xs @ ys)"
    3.16 +
    3.17 +primrec rev :: "'a list => 'a list" where
    3.18 +"rev []        = []" |
    3.19 +"rev (x # xs)  = (rev xs) @ (x # [])"
     4.1 --- a/src/Doc/Tutorial/ToyList/ToyList2	Sat May 24 19:15:04 2014 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,21 +0,0 @@
     4.4 -lemma app_Nil2 [simp]: "xs @ [] = xs"
     4.5 -apply(induct_tac xs)
     4.6 -apply(auto)
     4.7 -done
     4.8 -
     4.9 -lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
    4.10 -apply(induct_tac xs)
    4.11 -apply(auto)
    4.12 -done
    4.13 -
    4.14 -lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
    4.15 -apply(induct_tac xs)
    4.16 -apply(auto)
    4.17 -done
    4.18 -
    4.19 -theorem rev_rev [simp]: "rev(rev xs) = xs"
    4.20 -apply(induct_tac xs)
    4.21 -apply(auto)
    4.22 -done
    4.23 -
    4.24 -end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Doc/Tutorial/ToyList/ToyList2.txt	Sat May 24 20:07:26 2014 +0200
     5.3 @@ -0,0 +1,21 @@
     5.4 +lemma app_Nil2 [simp]: "xs @ [] = xs"
     5.5 +apply(induct_tac xs)
     5.6 +apply(auto)
     5.7 +done
     5.8 +
     5.9 +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
    5.10 +apply(induct_tac xs)
    5.11 +apply(auto)
    5.12 +done
    5.13 +
    5.14 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
    5.15 +apply(induct_tac xs)
    5.16 +apply(auto)
    5.17 +done
    5.18 +
    5.19 +theorem rev_rev [simp]: "rev(rev xs) = xs"
    5.20 +apply(induct_tac xs)
    5.21 +apply(auto)
    5.22 +done
    5.23 +
    5.24 +end
     6.1 --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat May 24 19:15:04 2014 +0200
     6.2 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat May 24 20:07:26 2014 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4    let
     6.5      val texts =
     6.6        map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
     6.7 -        ["ToyList1", "ToyList2"];
     6.8 +        ["ToyList1.txt", "ToyList2.txt"];
     6.9      val trs = Outer_Syntax.parse Position.start (implode texts);
    6.10      val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
    6.11    in @{assert} (Toplevel.is_toplevel end_state) end;
     7.1 --- a/src/Doc/Tutorial/document/fp.tex	Sat May 24 19:15:04 2014 +0200
     7.2 +++ b/src/Doc/Tutorial/document/fp.tex	Sat May 24 20:07:26 2014 +0200
     7.3 @@ -26,7 +26,7 @@
     7.4  
     7.5  \begin{figure}[htbp]
     7.6  \begin{ttbox}\makeatother
     7.7 -\input{ToyList1}\end{ttbox}
     7.8 +\input{ToyList1.txt}\end{ttbox}
     7.9  \caption{A Theory of Lists}
    7.10  \label{fig:ToyList}
    7.11  \end{figure}
    7.12 @@ -44,7 +44,7 @@
    7.13  
    7.14  \begin{figure}[htbp]
    7.15  \begin{ttbox}\makeatother
    7.16 -\input{ToyList2}\end{ttbox}
    7.17 +\input{ToyList2.txt}\end{ttbox}
    7.18  \caption{Proofs about Lists}
    7.19  \label{fig:ToyList-proofs}
    7.20  \end{figure}