1.1 --- a/doc-src/ROOT	Tue Aug 28 15:00:05 2012 +0200
     1.2 +++ b/doc-src/ROOT	Tue Aug 28 15:07:43 2012 +0200
     1.3 @@ -343,8 +343,28 @@
     1.4      "../proof.sty"
     1.5      "../ttbox.sty"
     1.6      "../manual.bib"
     1.7 +    "document/advanced0.tex"
     1.8 +    "document/appendix0.tex"
     1.9 +    "document/basics.tex"
    1.10 +    "document/build"
    1.11 +    "document/cl2emono-modified.sty"
    1.12 +    "document/ctl0.tex"
    1.13 +    "document/documents0.tex"
    1.14 +    "document/fp.tex"
    1.15 +    "document/inductive0.tex"
    1.16 +    "document/isa-index"
    1.17 +    "document/Isa-logics.eps"
    1.18 +    "document/Isa-logics.pdf"
    1.19 +    "document/numerics.tex"
    1.20      "document/pghead.eps"
    1.21      "document/pghead.pdf"
    1.22 -    "document/build"
    1.23 +    "document/preface.tex"
    1.24 +    "document/protocol.tex"
    1.25      "document/root.tex"
    1.26 +    "document/rules.tex"
    1.27 +    "document/sets.tex"
    1.28 +    "document/tutorial.sty"
    1.29 +    "document/typedef.pdf"
    1.30 +    "document/typedef.ps"
    1.31 +    "document/types0.tex"
    1.32  

     2.1 --- a/doc-src/TutorialI/document/build	Tue Aug 28 15:00:05 2012 +0200
     2.2 +++ b/doc-src/TutorialI/document/build	Tue Aug 28 15:07:43 2012 +0200
     2.3 @@ -22,7 +22,7 @@
     2.4  "$ISABELLE_TOOL" latex -o bbl
     2.5  "$ISABELLE_TOOL" latex -o "$FORMAT"
     2.6  "$ISABELLE_TOOL" latex -o "$FORMAT"
     2.7 -"$ISABELLE_HOME/doc-src/sedindex" root
     2.8 +./isa-index root
     2.9  [ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
    2.10  "$ISABELLE_TOOL" latex -o "$FORMAT"
    2.11  "$ISABELLE_TOOL" latex -o "$FORMAT"

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/TutorialI/document/isa-index	Tue Aug 28 15:07:43 2012 +0200
     3.3 @@ -0,0 +1,23 @@
     3.4 +#! /bin/sh
     3.5 +#
     3.6 +#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
     3.7 +#
     3.8 +#  puts strings prefixed by * into \tt font
     3.9 +#    terminator characters for strings are |!@{}
    3.10 +#
    3.11 +# a space terminates the \tt part to allow \index{*notE theorem}, etc.
    3.12 +#
    3.13 +# note that makeindex uses a dboule quote (") to delimit special characters.
    3.14 +#
    3.15 +# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
    3.16 +# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
    3.17 +# change *"X"Y      to  "X"Y@{\tt "X"Y}
    3.18 +# change *"X        to  "X@{\tt "X}
    3.19 +# change *IDENT  to  IDENT@{\tt IDENT}  
    3.20 +#    where IDENT is any string not containing | ! or @
    3.21 +# FOUR backslashes: to escape the shell AND sed
    3.22 +sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
    3.23 +s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
    3.24 +s~\*\(\".\".\)~\1@\\\\isa {\1}~g
    3.25 +s~\*\(\".\)~\1@\\\\isa {\1}~g
    3.26 +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind

     4.1 --- a/doc-src/TutorialI/isa-index	Tue Aug 28 15:00:05 2012 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,23 +0,0 @@
     4.4 -#! /bin/sh
     4.5 -#
     4.6 -#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
     4.7 -#
     4.8 -#  puts strings prefixed by * into \tt font
     4.9 -#    terminator characters for strings are |!@{}
    4.10 -#
    4.11 -# a space terminates the \tt part to allow \index{*notE theorem}, etc.
    4.12 -#
    4.13 -# note that makeindex uses a dboule quote (") to delimit special characters.
    4.14 -#
    4.15 -# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
    4.16 -# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
    4.17 -# change *"X"Y      to  "X"Y@{\tt "X"Y}
    4.18 -# change *"X        to  "X@{\tt "X}
    4.19 -# change *IDENT  to  IDENT@{\tt IDENT}  
    4.20 -#    where IDENT is any string not containing | ! or @
    4.21 -# FOUR backslashes: to escape the shell AND sed
    4.22 -sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
    4.23 -s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
    4.24 -s~\*\(\".\".\)~\1@\\\\isa {\1}~g
    4.25 -s~\*\(\".\)~\1@\\\\isa {\1}~g
    4.26 -s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind