src/Doc/Codegen/Evaluation.thy
changeset 58310 91ea607a34d8
parent 58305 57752a91eec4
child 58620 7435b6a3f72e
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4    An simplistic example:
     1.5  *}
     1.6  
     1.7 -datatype_new %quote form_ord = T | F | Less nat nat
     1.8 +datatype %quote form_ord = T | F | Less nat nat
     1.9    | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
    1.10  
    1.11  primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
    1.12 @@ -259,7 +259,7 @@
    1.13    example:
    1.14  *}
    1.15  
    1.16 -datatype_new %quote form = T | F | And form form | Or form form (*<*)
    1.17 +datatype %quote form = T | F | And form form | Or form form (*<*)
    1.18  
    1.19  (*>*) ML %quotett {*
    1.20    fun eval_form @{code T} = true