doc-src/System/Thy/document/Scala.tex

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

%
\begin{isabellebody}%
\def\isabellecontext{Scala}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Scala\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Isabelle/Scala development tools%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle/ML and Isabelle/Scala are the two main language
environments for Isabelle tool implementations.  There are some basic
command-line tools to work with the underlying Java Virtual Machine,
the Scala toplevel and compiler.  Note that Isabelle/jEdit
(\secref{sec:tool-tty}) provides a Scala Console for interactive
experimentation within the running application.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for
  the Java Runtime Environment, within the regular Isabelle settings
  environment (\secref{sec:settings}).  The command line arguments are
  that of the underlying Java version.  It is run in \verb|-server| mode if possible, to improve performance (at the cost of
  extra startup time).

  The \verb|java| executable is the one within \hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, according to the standard directory layout for
  official JDK distributions.  The class loader is augmented such that
  the name space of \verb|Isabelle/Pure.jar| is available,
  which is the main Isabelle/Scala module.

  For example, the following command-line invokes the main method of
  class \verb|isabelle.GUI_Setup|, which opens a windows with
  some diagnostic information about the Isabelle environment:
\begin{alltt}
  isabelle java isabelle.GUI_Setup
\end{alltt}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Scala toplevel \label{sec:tool-scala}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for
  the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above.  The command line
  arguments are that of the underlying Scala version.

  This allows to interact with Isabelle/Scala in TTY mode like this:
\begin{alltt}
  isabelle scala
  scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
  scala> isabelle.Isabelle_System.find_logics()
\end{alltt}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Scala compiler \label{sec:tool-scalac}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper
  for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above.  The command
  line arguments are that of the underlying Scala version.

  This allows to compile further Scala modules, depending on existing
  Isabelle/Scala functionality.  The resulting class or jar files can
  be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath|
  Bash function that is provided by the Isabelle process environment.
  Thus add-on components can register themselves in a modular manner,
  see also \secref{sec:components}.

  Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
  adding plugin components, which needs special attention since
  it overrides the standard Java class loader.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: