--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:02 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:08 2014 +0200
@@ -507,7 +507,8 @@
\item
The @{text "plugins"} option indicates which plugins should be enabled
-(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
+(@{text only}) or disabled (@{text del}). Wildcards (``@{text *}'') are allowed
+(e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
\item
The @{text "discs_sels"} option indicates that discriminators and selectors
@@ -539,7 +540,7 @@
The optional names preceding the type variables allow to override the default
names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
arguments can be marked as dead by entering @{text dead} in front of the
-type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
+type variable (e.g., @{text "(dead 'a)"}); otherwise, they are live or dead
(and a set function is generated or not) depending on where they occur in the
right-hand sides of the definition. Declaring a type argument as dead can speed
up the type definition but will prevent any later (co)recursion through that
@@ -2652,7 +2653,7 @@
parenthesized mixfix notation \cite{isabelle-isar-ref}.
Type arguments are live by default; they can be marked as dead by entering
-@{text dead} in front of the type variable (e.g., ``@{text "(dead 'a)"}'')
+@{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
instead of an identifier for the corresponding set function. Witnesses can be
specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
is identical to the left-hand side of a @{command datatype_new} or
@@ -2843,9 +2844,9 @@
text {*
The integration of (co)datatypes with Quickcheck is accomplished by a number of
-plugins that instantiate specific type classes: @{text random},
-@{text exhaustive}, @{text bounded_forall}, @{text full_exhaustive}, and
-@{text narrowing}.
+plugins that instantiate specific type classes: @{text quickcheck_random},
+@{text quickcheck_exhaustive}, @{text quickcheck_bounded_forall},
+@{text quickcheck_full_exhaustive}, and @{text quickcheck_narrowing}.
*}
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 08 14:03:08 2014 +0200
@@ -35,7 +35,7 @@
(binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
(term list * thm list) * theory
val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
- local_theory -> (string list * (term list * (int list * thm list))) * local_theory
+ local_theory -> (string list * (term list * thm list)) * local_theory
end;
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -516,7 +516,7 @@
val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
-val add_primrec_simple = apfst (apsnd (apsnd (apsnd flat o apfst flat))) ooo
+val add_primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo
BNF_LFP_Rec_Sugar.add_primrec_simple;
val _ =
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Sep 08 14:03:08 2014 +0200
@@ -529,7 +529,11 @@
error ("primrec error:\n " ^ str ^ "\nin\n " ^
space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns));
-val add_primrec_simple = add_primrec_simple' [];
+fun add_primrec_simple fixes ts lthy =
+ add_primrec_simple' [] fixes ts lthy
+ handle OLD_PRIMREC () =>
+ Old_Primrec.add_primrec_simple fixes ts lthy
+ |>> apsnd (apsnd (pair [] o single)) o apfst single;
fun gen_primrec old_primrec prep_spec opts
(raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Sep 08 14:03:08 2014 +0200
@@ -92,7 +92,19 @@
structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
struct
-fun map_prod f g (x, y) = (f x, g y)
+fun match_entire_string pat s =
+ let
+ fun match [] [] = true
+ | match [] _ = false
+ | match (ps as #"*" :: ps') cs =
+ match ps' cs orelse (not (null cs) andalso match ps (tl cs))
+ | match _ [] = false
+ | match (p :: ps) (c :: cs) = p = c andalso match ps cs;
+ in
+ match (String.explode pat) (String.explode s)
+ end;
+
+fun map_prod f g (x, y) = (f x, g y);
fun map3 _ [] [] [] = []
| map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
@@ -272,7 +284,8 @@
val parse_plugins =
Parse.reserved "plugins" |--
((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"}
- -- Scan.repeat Parse.short_ident) >> (fn (modif, ss) => modif o member (op =) ss);
+ -- Scan.repeat (Parse.short_ident || Parse.string))
+ >> (fn (modif, pats) => modif o member (uncurry match_entire_string o swap) pats);
fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
@@ -291,7 +304,6 @@
let val (butlast, last) = split_last xs;
in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
-(*not eta-converted because of monotype restriction*)
fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;