Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use 'datatype_new'
authorblanchet
Wed, 03 Sep 2014 00:06:25 +0200
changeset 58153 ca7ea280e906
parent 58152 6fe60a9a5bad
child 58154 47c3c7019b97
use 'datatype_new'
src/HOL/Extraction.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction.thy	Wed Sep 03 00:06:24 2014 +0200
+++ b/src/HOL/Extraction.thy	Wed Sep 03 00:06:25 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 sumbool = Left | Right
+datatype_new sumbool = Left | Right
 
 subsection {* Type of extracted program *}
isabelle