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