src/HOL/Extraction.thy
changeset 58153 ca7ea280e906
parent 58112 8081087096ad
child 58310 91ea607a34d8
     1.1 --- a/src/HOL/Extraction.thy	Wed Sep 03 00:06:24 2014 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Wed Sep 03 00:06:25 2014 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     1.5    induct_true_def induct_false_def
     1.6  
     1.7 -datatype sumbool = Left | Right
     1.8 +datatype_new sumbool = Left | Right
     1.9  
    1.10  subsection {* Type of extracted program *}
    1.11