1.1 --- a/doc-src/ROOT	Mon Jul 30 17:25:45 2012 +0200
     1.2 +++ b/doc-src/ROOT	Mon Jul 30 17:37:34 2012 +0200
     1.3 @@ -177,6 +177,10 @@
     1.4      "Sets/Relations"
     1.5      "Sets/Recur"
     1.6  
     1.7 +session ToyList2 (doc) in "TutorialI/ToyList2" = HOL +
     1.8 +  options [browser_info = false, document = false, print_mode = "brackets"]
     1.9 +  theories ToyList
    1.10 +
    1.11  session examples (doc) in "ZF" = ZF +
    1.12    options [browser_info = false, document = false,
    1.13      document_dump = document, document_dump_mode = "tex",

     2.1 --- a/doc-src/TutorialI/Makefile	Mon Jul 30 17:25:45 2012 +0200
     2.2 +++ b/doc-src/TutorialI/Makefile	Mon Jul 30 17:37:34 2012 +0200
     2.3 @@ -23,9 +23,13 @@
     2.4  	../../lib/texinputs/isabelle.sty				\
     2.5  	../../lib/texinputs/isabellesym.sty ../pdfsetup.sty
     2.6  
     2.7 +ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
     2.8 +	cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
     2.9 +
    2.10 +
    2.11  dvi: $(NAME).dvi
    2.12  
    2.13 -$(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps
    2.14 +$(NAME).dvi: $(FILES) isabelle_hol.eps typedef.ps ToyList2/ToyList.thy
    2.15  	$(LATEX) $(NAME)
    2.16  	$(BIBTEX) $(NAME)
    2.17  	$(LATEX) $(NAME)
    2.18 @@ -35,7 +39,7 @@
    2.19  
    2.20  pdf: $(NAME).pdf
    2.21  
    2.22 -$(NAME).pdf: $(FILES) isabelle_hol.pdf typedef.pdf
    2.23 +$(NAME).pdf: $(FILES) isabelle_hol.pdf typedef.pdf ToyList2/ToyList.thy
    2.24  	$(PDFLATEX) $(NAME)
    2.25  	$(BIBTEX) $(NAME)
    2.26  	$(PDFLATEX) $(NAME)

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/TutorialI/ToyList2/ToyList.thy	Mon Jul 30 17:37:34 2012 +0200
     3.3 @@ -0,0 +1,37 @@
     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 # [])"
    3.20 +lemma app_Nil2 [simp]: "xs @ [] = xs"
    3.21 +apply(induct_tac xs)
    3.22 +apply(auto)
    3.23 +done
    3.24 +
    3.25 +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
    3.26 +apply(induct_tac xs)
    3.27 +apply(auto)
    3.28 +done
    3.29 +
    3.30 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
    3.31 +apply(induct_tac xs)
    3.32 +apply(auto)
    3.33 +done
    3.34 +
    3.35 +theorem rev_rev [simp]: "rev(rev xs) = xs"
    3.36 +apply(induct_tac xs)
    3.37 +apply(auto)
    3.38 +done
    3.39 +
    3.40 +end