src/HOL/Extraction.thy
changeset 58335 a5a3b576fcfb
parent 58334 7553a1bcecb7
child 58343 1defb39ab329
     1.1 --- a/src/HOL/Extraction.thy	Sun Sep 14 22:59:30 2014 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Mon Sep 15 10:49:07 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 (plugins only: code) sumbool = Left | Right
     1.8 +datatype (plugins only:) sumbool = Left | Right
     1.9  
    1.10  subsection {* Type of extracted program *}
    1.11