author | blanchet |
Wed Sep 03 00:06:25 2014 +0200 (2014-09-03) | |
changeset 58153 | ca7ea280e906 |
parent 58152 | 6fe60a9a5bad |
child 58154 | 47c3c7019b97 |
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