Quelle  README

Lightweight├
==========

Information.texlj_baseott .ott
- LJ
Please the Isabelle PDF and

    http//rok.strnisa.comlj


Overview----------
--------------

├java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
                   createPDF thedocument.")
├── Lightweight_
                                        definition of LJ.")
├── Lightweight_Java_Equivalence.thy  ("Some equivalence functions based
                                        on the definition.")
├── Lightweight_Java_Proof.thy        ("A type soundness proof for LJ.")
├── README  ("This file.")
├── ROOT.ML  ("A file directing Isabelle which theories to compile.")
├── config  ("AFP maintenance configuration file.")
├── document
│   ├── root.bib  ("BibTeX bibliography for the 'root.tex'.")
│   └── root.tex  ("LaTeX source for generating the PDF overviewing LJ.")
└── ott-src  ("LJ's Ott source files provided for reference.")
    ├── Makefile
    ├── README
    ├── lj.ott
    ├── lj.tex
    ├── lj_base.ott
    └── lj_common.ott


Maintaining LJ
--------------

- Lightweight_Java_Definition.thy

Since "Lightweight_Java_Definition.thy" is generated by Ott, it should _not_
be modified directly. Please either:

1) E-mail the main author (rok@strnisa.com) to sort out any problem; or,

2) Modify the provided Ott-source files to obtain the desired result. Please
   notify the main author (rok@strnisa.com) of any such changes.


- Lightweight_Java_Equivalence.thy and Lightweight_Java_Proof.thy

These two files can be modified at will, as long as the semantics of "progress"
and "wf_preservation" is preserved.