doc-src/Codegen/Thy/document/Introduction.tex
changeset 30227 853abb4853cc
parent 30226 2f4684e2ea95
child 30836 1344132160bb
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Mar 03 13:20:53 2009 +0100
@@ -18,10 +18,6 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Code generation from \isa{Isabelle{\isacharslash}HOL} theories%
-}
-\isamarkuptrue%
-%
 \isamarkupsection{Introduction and Overview%
 }
 \isamarkuptrue%