Isabelle installation notes===========================1) System installation----------------------The Isabelle distribution includes both complete sources andprecompiled binary packages for common Unix-like platforms.Quick installation------------------Ready-to-go packages are provided for the ML compiler and runtimesystem, the Isabelle sources, and some major object-logics. A minimalsite installation of Isabelle on Linux/x86 works like this: tar -C /usr/local -xzf Isabelle.tar.gz tar -C /usr/local -xzf polyml.tar.gz tar -C /usr/local -xzf HOL_x86-linux.tar.gzThe install prefix given above may be changed as appropriate; there isno need to install into a system directory like /usr/local at all. Bydefault the ML system (and other contributed packages) are expected inany of the following locations: 1) [ISABELLE_HOME]/contrib 2) [ISABELLE_HOME]/.. 4) /usr/local 3) /usr/share 5) /optThis may be changed by editing [ISABELLE_HOME]/etc/settings manually.The installation may be finished as follows: cd [ISABELLE_HOME] ./bin/isabelle install -p /usr/local/binThe install utility creates global references to the present Isabelleinstallation, enabling users to invoke the Isabelle executableswithout explicit path names. This is the only place where a staticreference to [ISABELLE_HOME] is created; thus isabelle install has tobe run again whenever the Isabelle distribution is moved later.Compiling logics----------------The Isabelle.tar.gz archive already contains all Isabelle sources (anddocumentation). Precompiled object-logics are provided forconvenience.Assuming proper configuration of the underlying ML system(cf. Isabelle's etc/settings), further object-logics may be compiledlike this: [ISABELLE_HOME]/build FOLSpecial object-logic targets may be specified as follows: [ISABELLE_HOME]/build -m HOL-Algebra HOL2) User installation--------------------Running the Isabelle binaries-----------------------------Users may invoke the main Isabelle binaries (isabelle andisabelle-process) directly from their location within the distributiondirectory [ISABELLE_HOME] like this: [ISABELLE_HOME]/bin/isabelle tty -l HOLThis starts an interactive Isabelle session within the current textterminal. [ISABELLE_HOME]/bin may be put into the shell's searchPATH. An alternative is to create global references to the Isabelleexecutables as follows: [ISABELLE_HOME]/bin/isabelle install -p ~/binNote that the site-wide Isabelle installation may already provideIsabelle executables in some global bin directory (such as/usr/local/bin).