# HG changeset patch # User wenzelm # Date 1397212812 -7200 # Node ID 3ff16a7f0b2ebd1567c7ee8e78776710544485a1 # Parent cd8b6d849b6a7b9957fecddf03c63c08ec3e1554 more formal dependencies via 'document_files'; diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Classes/document/build --- a/src/Doc/Classes/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Classes/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Codegen/document/build --- a/src/Doc/Codegen/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Codegen/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Datatypes/document/build --- a/src/Doc/Datatypes/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Datatypes/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -5,10 +5,5 @@ FORMAT="$1" VARIANT="$2" -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Functions/document/build --- a/src/Doc/Functions/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Functions/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -5,10 +5,5 @@ FORMAT="$1" VARIANT="$2" -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Implementation/document/build --- a/src/Doc/Implementation/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Implementation/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,13 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Intro/document/build --- a/src/Doc/Intro/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Intro/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Isar_Ref/document/build --- a/src/Doc/Isar_Ref/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Isar_Ref/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,15 +6,6 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - ./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/JEdit/document/build --- a/src/Doc/JEdit/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/JEdit/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,14 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo jEdit - -cp "$ISABELLE_HOME/src/Doc/Isar_Ref/document/style.sty" . -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Logics/document/build --- a/src/Doc/Logics/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Logics/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Logics_ZF/document/build --- a/src/Doc/Logics_ZF/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Logics_ZF/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo ZF - -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . -cp "$ISABELLE_HOME/src/Doc/Logics/document/syntax.tex" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Main/document/build --- a/src/Doc/Main/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Main/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -5,9 +5,6 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" latex -o sty -cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" . - "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Nitpick/document/build --- a/src/Doc/Nitpick/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Nitpick/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,9 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Nitpick - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Prog_Prove/document/build --- a/src/Doc/Prog_Prove/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Prog_Prove/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,8 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo HOL - -cp "$ISABELLE_HOME/src/Doc/Prog_Prove/MyList.thy" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/ROOT --- a/src/Doc/ROOT Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/ROOT Fri Apr 11 12:40:12 2014 +0200 @@ -4,16 +4,17 @@ options [document_variants = "classes", quick_and_dirty] theories [document = false] Setup theories Classes - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Codegen (doc) in "Codegen" = "HOL-Library" + options [document_variants = "codegen", print_mode = "no_brackets,iff"] @@ -26,61 +27,68 @@ Evaluation Adaptation Further - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Datatypes (doc) in "Datatypes" = HOL + options [document_variants = "datatypes"] theories [document = false] Setup theories Datatypes - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Functions (doc) in "Functions" = HOL + options [document_variants = "functions", skip_proofs = false, quick_and_dirty] theories Functions - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/conclusion.tex" - "document/intro.tex" - "document/mathpartir.sty" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "conclusion.tex" + "intro.tex" + "mathpartir.sty" + "root.tex" + "style.sty" session Intro (doc) in "Intro" = Pure + options [document_variants = "intro"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../ttbox.sty" - "../manual.bib" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "ttbox.sty" + "manual.bib" + document_files + "advanced.tex" + "build" + "foundations.tex" + "getting.tex" + "root.tex" session Implementation (doc) in "Implementation" = "HOL-Proofs" + options [document_variants = "implementation"] @@ -96,18 +104,19 @@ Tactic theories [parallel_proofs = 0] Logic - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../ttbox.sty" - "../underscore.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "ttbox.sty" + "underscore.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Isar_Ref (doc) in "Isar_Ref" = HOL + options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] @@ -127,41 +136,48 @@ Quick_Reference Symbols ML_Tactic - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../ttbox.sty" - "../underscore.sty" - "../manual.bib" - "document/build" - "document/isar-vm.pdf" - "document/isar-vm.svg" - "document/root.tex" - "document/showsymbols" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "ttbox.sty" + "underscore.sty" + "manual.bib" + document_files + "build" + "isar-vm.pdf" + "isar-vm.svg" + "root.tex" + "showsymbols" + "style.sty" session JEdit (doc) in "JEdit" = HOL + options [document_variants = "jedit", thy_output_source] theories JEdit - files - "../Isar_Ref/document/style.sty" - "../extra.sty" - "../iman.sty" - "../isar.sty" - "../manual.bib" - "../pdfsetup.sty" - "../prepare_document" - "../ttbox.sty" - "../underscore.sty" - "document/build" - "document/isabelle-jedit.png" - "document/popup1.png" - "document/popup2.png" - "document/root.tex" + document_files (in "..") + "extra.sty" + "iman.sty" + "isar.sty" + "manual.bib" + "pdfsetup.sty" + "prepare_document" + "ttbox.sty" + "underscore.sty" + document_files (in "../Isar_Ref/document") + "style.sty" + document_files + "auto-tools.png" + "build" + "find.png" + "isabelle-jedit.png" + "output.png" + "popup1.png" + "popup2.png" + "root.tex" + "sledgehammer.png" session Sugar (doc) in "Sugar" = HOL + options [document_variants = "sugar"] @@ -169,13 +185,14 @@ "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar" theories Sugar - files - "../prepare_document" - "../pdfsetup.sty" - "document/build" - "document/mathpartir.sty" - "document/root.bib" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "build" + "mathpartir.sty" + "root.bib" + "root.tex" session Locales (doc) in "Locales" = HOL + options [document_variants = "locales", pretty_margin = 65, skip_proofs = false] @@ -183,30 +200,33 @@ Examples1 Examples2 Examples3 - files - "../prepare_document" - "../pdfsetup.sty" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "build" + "root.bib" + "root.tex" session Logics (doc) in "Logics" = Pure + options [document_variants = "logics"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../ttbox.sty" - "../manual.bib" - "document/CTT.tex" - "document/HOL.tex" - "document/LK.tex" - "document/Sequents.tex" - "document/build" - "document/preface.tex" - "document/root.tex" - "document/syntax.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "ttbox.sty" + "manual.bib" + document_files + "CTT.tex" + "HOL.tex" + "LK.tex" + "Sequents.tex" + "build" + "preface.tex" + "root.tex" + "syntax.tex" session Logics_ZF (doc) in "Logics_ZF" = ZF + options [document_variants = "logics-ZF", print_mode = "brackets", @@ -217,35 +237,42 @@ ZF_examples If ZF_Isar - files - "../prepare_document" - "../pdfsetup.sty" - "../isar.sty" - "../ttbox.sty" - "../manual.bib" - "../Logics/document/syntax.tex" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "isar.sty" + "ttbox.sty" + "manual.bib" + document_files (in "../Logics/document") + "syntax.tex" + document_files + "FOL.tex" + "ZF.tex" + "build" + "logics.sty" + "root.tex" session Main (doc) in "Main" = HOL + options [document_variants = "main"] theories Main_Doc - files - "../prepare_document" - "../pdfsetup.sty" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "build" + "root.tex" session Nitpick (doc) in "Nitpick" = Pure + options [document_variants = "nitpick"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../manual.bib" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "manual.bib" + document_files + "build" + "root.tex" session Prog_Prove (doc) in "Prog_Prove" = HOL + options [document_variants = "prog-prove", show_question_marks = false] @@ -256,28 +283,32 @@ Types_and_funs Logic Isar - files - "../prepare_document" - "../pdfsetup.sty" - "document/bang.pdf" - "document/build" - "document/intro-isabelle.tex" - "document/mathpartir.sty" - "document/prelude.tex" - "document/root.bib" - "document/root.tex" - "document/svmono.cls" + document_files (in ".") + "MyList.thy" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "bang.pdf" + "build" + "intro-isabelle.tex" + "mathpartir.sty" + "prelude.tex" + "root.bib" + "root.tex" + "svmono.cls" session Sledgehammer (doc) in "Sledgehammer" = Pure + options [document_variants = "sledgehammer"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../manual.bib" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "manual.bib" + document_files + "build" + "root.tex" session System (doc) in "System" = Pure + options [document_variants = "system", thy_output_source] @@ -288,19 +319,21 @@ Presentation Scala Misc - files - "../prepare_document" - "../Isar_Ref/document/style.sty" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../ttbox.sty" - "../underscore.sty" - "../manual.bib" - "document/browser_screenshot.png" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "ttbox.sty" + "underscore.sty" + "manual.bib" + document_files (in "../Isar_Ref/document") + "style.sty" + document_files + "browser_screenshot.png" + "build" + "root.tex" session Tutorial (doc) in "Tutorial" = HOL + options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] @@ -363,31 +396,33 @@ "Sets/Functions" "Sets/Relations" "Sets/Recur" - files - "ToyList/ToyList1" - "ToyList/ToyList2" - "../pdfsetup.sty" - "../ttbox.sty" - "../manual.bib" - "document/advanced0.tex" - "document/appendix0.tex" - "document/basics.tex" - "document/build" - "document/cl2emono-modified.sty" - "document/ctl0.tex" - "document/documents0.tex" - "document/fp.tex" - "document/inductive0.tex" - "document/isa-index" - "document/Isa-logics.pdf" - "document/numerics.tex" - "document/pghead.pdf" - "document/preface.tex" - "document/protocol.tex" - "document/root.tex" - "document/rules.tex" - "document/sets.tex" - "document/tutorial.sty" - "document/typedef.pdf" - "document/types0.tex" + document_files (in "ToyList") + "ToyList1" + "ToyList2" + document_files (in "..") + "pdfsetup.sty" + "ttbox.sty" + "manual.bib" + document_files + "advanced0.tex" + "appendix0.tex" + "basics.tex" + "build" + "cl2emono-modified.sty" + "ctl0.tex" + "documents0.tex" + "fp.tex" + "inductive0.tex" + "isa-index" + "Isa-logics.pdf" + "numerics.tex" + "pghead.pdf" + "preface.tex" + "protocol.tex" + "root.tex" + "rules.tex" + "sets.tex" + "tutorial.sty" + "typedef.pdf" + "types0.tex" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Sledgehammer/document/build --- a/src/Doc/Sledgehammer/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Sledgehammer/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,9 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H" - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/System/document/build --- a/src/Doc/System/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/System/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,14 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/Isar_Ref/document/style.sty" . -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r cd8b6d849b6a -r 3ff16a7f0b2e src/Doc/Tutorial/document/build --- a/src/Doc/Tutorial/document/build Fri Apr 11 11:52:28 2014 +0200 +++ b/src/Doc/Tutorial/document/build Fri Apr 11 12:40:12 2014 +0200 @@ -6,16 +6,6 @@ VARIANT="$2" "$ISABELLE_TOOL" logo HOL - -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - -cp "$ISABELLE_HOME/src/Doc/Tutorial/ToyList/ToyList1" . -cp "$ISABELLE_HOME/src/Doc/Tutorial/ToyList/ToyList2" . - -"$ISABELLE_TOOL" latex -o sty -cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" . - "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl ./isa-index root