diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/document/root.tex
--- 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}