equal
deleted
inserted
replaced
457 |
457 |
458 Build object-logic or run examples. Also creates browsing |
458 Build object-logic or run examples. Also creates browsing |
459 information (HTML etc.) according to settings. |
459 information (HTML etc.) according to settings. |
460 |
460 |
461 ISABELLE_USEDIR_OPTIONS= |
461 ISABELLE_USEDIR_OPTIONS= |
462 HOL_USEDIR_OPTIONS= |
|
463 |
462 |
464 ML_PLATFORM=x86-linux |
463 ML_PLATFORM=x86-linux |
465 ML_HOME=/usr/local/polyml-5.2.1/x86-linux |
464 ML_HOME=/usr/local/polyml-5.2.1/x86-linux |
466 ML_SYSTEM=polyml-5.2.1 |
465 ML_SYSTEM=polyml-5.2.1 |
467 ML_OPTIONS=-H 500 |
466 ML_OPTIONS=-H 500 |
472 call. Since the @{verbatim IsaMakefile}s of all object-logics |
471 call. Since the @{verbatim IsaMakefile}s of all object-logics |
473 distributed with Isabelle just invoke @{tool usedir} for the real |
472 distributed with Isabelle just invoke @{tool usedir} for the real |
474 work, one may control compilation options globally via above |
473 work, one may control compilation options globally via above |
475 variable. In particular, generation of \rmindex{HTML} browsing |
474 variable. In particular, generation of \rmindex{HTML} browsing |
476 information and document preparation is controlled here. |
475 information and document preparation is controlled here. |
477 |
|
478 The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the |
|
479 plain and main Isabelle/HOL images; its value is appended to |
|
480 @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions |
|
481 only. |
|
482 *} |
476 *} |
483 |
477 |
484 |
478 |
485 subsubsection {* Options *} |
479 subsubsection {* Options *} |
486 |
480 |