doc-src/Codegen/Thy/Further.thy

--- a/doc-src/Codegen/Thy/Further.thy	Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Tue Apr 07 08:52:43 2009 +0200
@@ -78,8 +78,9 @@
   with system code, the code generator provides a @{text code} antiquotation:
 *}
 
-datatype %quote form = T | F | And form form | Or form form
-ML %quotett {*
+datatype %quote form = T | F | And form form | Or form form (*<*)
+
+(*>*) ML %quotett {*
   fun eval_form @{code T} = true
     | eval_form @{code F} = false
     | eval_form (@{code And} (p, q)) =