| changeset 58310 | 91ea607a34d8 |
| parent 58153 | ca7ea280e906 |
| child 58334 | 7553a1bcecb7 |
--- a/src/HOL/Extraction.thy Thu Sep 11 19:26:59 2014 +0200 +++ b/src/HOL/Extraction.thy Thu Sep 11 19:32:36 2014 +0200 @@ -37,7 +37,7 @@ induct_forall_def induct_implies_def induct_equal_def induct_conj_def induct_true_def induct_false_def -datatype_new sumbool = Left | Right +datatype sumbool = Left | Right subsection {* Type of extracted program *}