Improved Java Module System (iJAM)
==================================

Making definitions from Ott source files
----------------------------------------

a) Get Ott source, make its native executable, and put it in your PATH. The
   source can be downloaded here:

      http://www.cl.cam.ac.uk/~pes20/ott/

   (The source Ott source files here were tested against version 0.20.1.)

b) Go into directory where Ott source files are located, and run "make". If you
   do not have the "make" command, run the following commands (assuming ott and
   pdflatex are in your PATH):

      ott -tex_wrap false -isabelle_inductive false \
          -o iJAM_included.tex -o iJAM.thy -merge true \
          lj_common.ott ljam_commoni.ott ljp_basei.ott \
          ljm_basei.ott ljami.ott
      pdflatex iJAM.tex

c) Generated files:
   - iJAM_included.tex
      LaTeX output of Ott. It is included in iJAM.tex, which is then compiled
      with pdflatex. (We do not generate a wrapped LaTex document directly,
      since some of our tex homs are context dependent.)
   - iJAM.pdf
      PDF version of the iJAM's definition.
   - iJAM.thy
      A valid Isabelle 2008 source containing Isabelle definition of iJAM.



More Information
----------------

More information and related documents can be found at:

  http://www.cl.cam.ac.uk/research/pls/javasem/iJAM/