src/HOL/Datatype.thy
changeset 25534 d0b74fdd6067
parent 25511 54db9b5080b8
child 25672 5850301e83c7
     1.1 --- a/src/HOL/Datatype.thy	Wed Dec 05 14:15:39 2007 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Dec 05 14:15:45 2007 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  
     1.5  theory Datatype
     1.6  imports Finite_Set
     1.7 -uses "Tools/datatype_codegen.ML"
     1.8  begin
     1.9  
    1.10  typedef (Node)
    1.11 @@ -682,8 +681,6 @@
    1.12  
    1.13  subsubsection {* Code generator setup *}
    1.14  
    1.15 -setup DatatypeCodegen.setup
    1.16 -
    1.17  definition
    1.18    is_none :: "'a option \<Rightarrow> bool" where
    1.19    is_none_none [code post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"