changeset 30227 | 853abb4853cc |
parent 30226 | 2f4684e2ea95 |
child 30880 | 257cbe43faa8 |
--- a/doc-src/Codegen/Thy/Further.thy Tue Mar 03 11:00:51 2009 +0100 +++ b/doc-src/Codegen/Thy/Further.thy Tue Mar 03 13:20:53 2009 +0100 @@ -79,8 +79,7 @@ *} datatype %quote form = T | F | And form form | Or form form - -ML %quote {* +ML %quotett {* fun eval_form @{code T} = true | eval_form @{code F} = false | eval_form (@{code And} (p, q)) =