equal
deleted
inserted
replaced
67 @{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>} |
67 @{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>} |
68 |
68 |
69 The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as |
69 The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as |
70 reported by the above verbose invocation of the build process. |
70 reported by the above verbose invocation of the build process. |
71 |
71 |
72 Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>) |
72 Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in |
73 also provide printable documents in PDF. These are prepared automatically as |
73 \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are |
74 well if enabled like this: |
74 prepared automatically as well if enabled like this: |
75 @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>} |
75 @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>} |
76 |
76 |
77 Enabling both browser info and document preparation simultaneously causes an |
77 Enabling both browser info and document preparation simultaneously causes an |
78 appropriate ``document'' link to be included in the HTML index. Documents |
78 appropriate ``document'' link to be included in the HTML index. Documents |
79 may be generated independently of browser information as well, see |
79 may be generated independently of browser information as well, see |