author | blanchet |
Mon, 15 Sep 2014 16:11:01 +0200 | |
changeset 58343 | 1defb39ab329 |
parent 58342 | 9a82544fd29f |
child 58344 | ea3d989219b4 |
--- a/src/HOL/Extraction.thy Mon Sep 15 14:31:32 2014 +0200 +++ b/src/HOL/Extraction.thy Mon Sep 15 16:11:01 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 (plugins only:) sumbool = Left | Right +datatype (plugins only: code) sumbool = Left | Right subsection {* Type of extracted program *}