Mercurialisabelle / changeset
summary | shortlog | changelog | graph | tags | branches | files | changeset | raw | gz
use 'datatype_new'
authorblanchet
Wed Sep 03 00:06:25 2014 +0200 (2014-09-03)
changeset 58153ca7ea280e906
parent 58152 6fe60a9a5bad
child 58154 47c3c7019b97
use 'datatype_new'
src/HOL/Extraction.thy file | annotate | diff | revisions 
     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
isabelle