INSTALL

Nicer names in FindTheorems.
* Patch NameSpace.get_accesses, contributed by Timothy Bourke:

NameSpace.get_accesses has been patched to fix the following
bug:
theory OverHOL imports Main begin
lemma conjI: "a & b --> b"
by blast

ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of;
val x1 = NameSpace.get_accesses ns "HOL.conjI";
val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *}
end

where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"],
but x1 should be just ["HOL.conjI"].

NameSpace.get_accesses is only used within the NameSpace
structure itself. The two uses have been modified to retain
their original behaviour.

Note that NameSpace.valid_accesses gives different results:
get_accesses ns "HOL.eq_class.eq"
gives ["eq", "eq_class.eq", "HOL.eq_class.eq"]
but,
valid_accesses ns "HOL.eq_class.eq"
gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"]

* Patch FindTheorems:
Prefer names that are shorter to type in the current context.

* Re-export space_of.

Isabelle installation notes
===========================

1) System installation
----------------------

The Isabelle distribution includes both complete sources and
precompiled binary packages for common Unix platforms.


Quick installation
------------------

Ready-to-go packages are provided for the ML compiler and runtime
system, the Isabelle sources, and some major object-logics.  A minimal
site installation of Isabelle on Linux/x86 works like this:

  tar -C /usr/local -xzf Isabelle.tar.gz
  tar -C /usr/local -xzf polyml_x86-linux.tar.gz
  tar -C /usr/local -xzf HOL_x86-linux.tar.gz

The install prefix given above may be changed as appropriate; there is
no need to install into a system directory like /usr/local at all.  By
default the ML system (and other contributed packages) are expected in
any of the following locations:

  1) [ISABELLE_HOME]/contrib
  2) [ISABELLE_HOME]/..
  4) /usr/local
  3) /usr/share
  5) /opt

This 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/bin

The install utility creates global references to the present Isabelle
installation, enabling users to invoke the Isabelle executables
without explicit path names.  This is the only place where a static
reference to [ISABELLE_HOME] is created; thus isabelle install has to
be run again whenever the Isabelle distribution is moved later.


Compiling logics
----------------

The Isabelle.tar.gz archive already contains all Isabelle sources (and
documentation).  Precompiled object-logics are provided for
convenience.

Assuming proper configuration of the underlying ML system
(cf. Isabelle's etc/settings), further object-logics may be compiled
like this:

  [ISABELLE_HOME]/build FOL

Special object-logic targets may be specified as follows:

  [ISABELLE_HOME]/build -m HOL-Algebra HOL


2) User installation
--------------------

Running the Isabelle binaries
-----------------------------

Users may invoke the main Isabelle binaries (isabelle and
isabelle-process) directly from their location within the distribution
directory [ISABELLE_HOME] like this:

  [ISABELLE_HOME]/bin/isabelle-process HOL

This starts an interactive Isabelle session within the current text
terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
PATH.  An alternative is to create global references to the Isabelle
executables as follows:

  [ISABELLE_HOME]/bin/isabelle install -p ~/bin

Note that the site-wide Isabelle installation may already provide
Isabelle executables in some global bin directory (such as
/usr/local/bin).