doc-src/TutorialI/tutorial.tex

 \documentclass{article}
 \usepackage{cl2emono-modified,isabelle,isabellesym}
 \usepackage{../proof,amsmath,amsfonts}
 \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
-\let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig  %bug in marvosym!?
+\usepackage[greek,english]{babel}
 \usepackage{../pdfsetup}   
 %last package!
 
 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
 %\remarksfalse