equal
deleted
inserted
replaced
20 |
20 |
21 "$ISABELLE_TOOL" latex -o "$FORMAT" |
21 "$ISABELLE_TOOL" latex -o "$FORMAT" |
22 "$ISABELLE_TOOL" latex -o bbl |
22 "$ISABELLE_TOOL" latex -o bbl |
23 "$ISABELLE_TOOL" latex -o "$FORMAT" |
23 "$ISABELLE_TOOL" latex -o "$FORMAT" |
24 "$ISABELLE_TOOL" latex -o "$FORMAT" |
24 "$ISABELLE_TOOL" latex -o "$FORMAT" |
25 "$ISABELLE_HOME/doc-src/sedindex" root |
25 ./isa-index root |
26 [ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out |
26 [ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out |
27 "$ISABELLE_TOOL" latex -o "$FORMAT" |
27 "$ISABELLE_TOOL" latex -o "$FORMAT" |
28 "$ISABELLE_TOOL" latex -o "$FORMAT" |
28 "$ISABELLE_TOOL" latex -o "$FORMAT" |