--- a/src/HOL/Bali/document/root.tex Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/document/root.tex Tue Jul 16 20:25:21 2002 +0200
@@ -152,6 +152,9 @@
for the maximal recursive depth. The semantics is not altered. The annotation
is needed for the soundness proof of the axiomatic semantics.
+\item[Trans]
+A smallstep operational semantics for JavaCard.
+
\item[AxSem]
An axiomatic semantics (Hoare logic) for JavaCard.
@@ -209,6 +212,8 @@
\chapter{Evaln}
\input{Evaln}
+\chapter{Trans}
+\input{Trans}
\chapter{AxSem}
\input{AxSem}
\chapter{AxSound}