--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Aug 18 17:42:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Aug 18 17:42:35 2011 +0200
@@ -157,8 +157,11 @@
\item @{text R.cases} is the case analysis (or elimination) rule;
\item @{text R.induct} or @{text R.coinduct} is the (co)induction
- rule.
-
+ rule;
+
+ \item @{text R.simps} is the equation unrolling the fixpoint of the
+ predicate one step.
+
\end{description}
When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Aug 18 17:42:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Aug 18 17:42:35 2011 +0200
@@ -225,8 +225,11 @@
\item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
\item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
- rule.
-
+ rule;
+
+ \item \isa{R{\isaliteral{2E}{\isachardot}}simps} is the equation unrolling the fixpoint of the
+ predicate one step.
+
\end{description}
When several predicates \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 17:42:18 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 17:42:35 2011 +0200
@@ -465,7 +465,7 @@
(* setup *)
-val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
+val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
val setup =
Code.datatype_interpretation ensure_partial_term_of
@@ -474,4 +474,4 @@
(((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
-end;
\ No newline at end of file
+end;