Lightweight Java (LJ)
=====================
Information about LJ
--------------------
Please see the Isabelle-generated PDF
and/or
http://rok.strnisa.com/lj/
Overview of files
-----------------
├── IsaMakefile (
"Isabelle makefile to verify the theories, and to
create a PDF within the 'document' directory.")
├── Lightweight_Java_Definition.thy (
"The Ott-generated Isabelle2011
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 Java (LJ)
├── Makefile
├─ README===========
├
├── lj
├── lj_base.
└──lj_common
Maintaining seethe-generated/or:/rok//
-----------
- 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 filescreate a within '' directory
and "wf_preservation" is preserved.
