--- a/src/HOL/Code_Evaluation.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Tue Sep 16 19:23:37 2014 +0200
@@ -13,7 +13,7 @@
subsubsection {* Terms and class @{text term_of} *}
-datatype (plugins only: code) "term" = dummy_term
+datatype (plugins only: code extraction) "term" = dummy_term
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
--- a/src/HOL/Enum.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Enum.thy Tue Sep 16 19:23:37 2014 +0200
@@ -493,7 +493,8 @@
text {* We define small finite types for use in Quickcheck *}
-datatype (plugins only: code "quickcheck*") finite_1 = a\<^sub>1
+datatype (plugins only: code "quickcheck*" extraction) finite_1 =
+ a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -595,7 +596,8 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype (plugins only: code "quickcheck*") finite_2 = a\<^sub>1 | a\<^sub>2
+datatype (plugins only: code "quickcheck*" extraction) finite_2 =
+ a\<^sub>1 | a\<^sub>2
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -701,7 +703,8 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype (plugins only: code "quickcheck*") finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype (plugins only: code "quickcheck*" extraction) finite_3 =
+ a\<^sub>1 | a\<^sub>2 | a\<^sub>3
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -825,7 +828,8 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype (plugins only: code "quickcheck*") finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype (plugins only: code "quickcheck*" extraction) finite_4 =
+ a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -926,7 +930,8 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-datatype (plugins only: code "quickcheck*") finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype (plugins only: code "quickcheck*" extraction) finite_5 =
+ a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
--- a/src/HOL/Extraction.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Extraction.thy Tue Sep 16 19:23:37 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: code) sumbool = Left | Right
+datatype (plugins only: code extraction) sumbool = Left | Right
subsection {* Type of extracted program *}
--- a/src/HOL/Lazy_Sequence.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy Tue Sep 16 19:23:37 2014 +0200
@@ -8,7 +8,8 @@
subsection {* Type of lazy sequences *}
-datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
+datatype (plugins only: code extraction) (dead 'a) lazy_sequence =
+ lazy_sequence_of_list "'a list"
primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
where
--- a/src/HOL/Nitpick.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Nitpick.thy Tue Sep 16 19:23:37 2014 +0200
@@ -14,9 +14,9 @@
"nitpick_params" :: thy_decl
begin
-datatype (plugins only:) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
-datatype (plugins only:) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
-datatype (plugins only:) (dead 'a) word = Word "'a set"
+datatype (plugins only: extraction) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype (plugins only: extraction) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
+datatype (plugins only: extraction) (dead 'a) word = Word "'a set"
typedecl bisim_iterator
typedecl unsigned_bit
--- a/src/HOL/Predicate.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Predicate.thy Tue Sep 16 19:23:37 2014 +0200
@@ -10,7 +10,7 @@
subsection {* The type of predicate enumerations (a monad) *}
-datatype (plugins only: code) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
+datatype (plugins only: code extraction) (dead 'a) pred = Pred "'a \<Rightarrow> bool"
primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
eval_pred: "eval (Pred f) = f"
@@ -402,7 +402,7 @@
subsection {* Implementation *}
-datatype (plugins only: code) (dead 'a) seq =
+datatype (plugins only: code extraction) (dead 'a) seq =
Empty
| Insert "'a" "'a pred"
| Join "'a pred" "'a seq"
--- a/src/HOL/Quickcheck_Exhaustive.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Sep 16 19:23:37 2014 +0200
@@ -574,8 +574,11 @@
where
"pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
-datatype (plugins only: code) (dead 'a) unknown = Unknown | Known 'a
-datatype (plugins only: code) (dead 'a) three_valued = Unknown_value | Value 'a | No_value
+datatype (plugins only: code extraction) (dead 'a) unknown =
+ Unknown | Known 'a
+
+datatype (plugins only: code extraction) (dead 'a) three_valued =
+ Unknown_value | Value 'a | No_value
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
--- a/src/HOL/Quickcheck_Narrowing.thy Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Tue Sep 16 19:23:37 2014 +0200
@@ -26,14 +26,14 @@
subsubsection {* Narrowing's deep representation of types and terms *}
-datatype (plugins only: code) narrowing_type =
+datatype (plugins only: code extraction) narrowing_type =
Narrowing_sum_of_products "narrowing_type list list"
-datatype (plugins only: code) narrowing_term =
+datatype (plugins only: code extraction) narrowing_term =
Narrowing_variable "integer list" narrowing_type
| Narrowing_constructor integer "narrowing_term list"
-datatype (plugins only: code) (dead 'a) narrowing_cons =
+datatype (plugins only: code extraction) (dead 'a) narrowing_cons =
Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
@@ -127,7 +127,7 @@
class narrowing =
fixes narrowing :: "integer => 'a narrowing_cons"
-datatype (plugins only: code) property =
+datatype (plugins only: code extraction) property =
Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
| Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term"
| Property bool
@@ -158,7 +158,7 @@
subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
-datatype (plugins only: code quickcheck_narrowing) (dead 'a, dead 'b) ffun =
+datatype (plugins only: code quickcheck_narrowing extraction) (dead 'a, dead 'b) ffun =
Constant 'b
| Update 'a 'b "('a, 'b) ffun"
@@ -170,7 +170,7 @@
hide_type (open) ffun
hide_const (open) Constant Update eval_ffun
-datatype (plugins only: code quickcheck_narrowing) (dead 'b) cfun = Constant 'b
+datatype (plugins only: code quickcheck_narrowing extraction) (dead 'b) cfun = Constant 'b
primrec eval_cfun :: "'b cfun => 'a => 'b"
where