# HG changeset patch
# User bulwahn
# Date 1333541304 -7200
# Node ID 803729c9fd4dc20b14110268d4b078321fd6fcab
# Parent  9a82999ebbd6c0f40fb4bbd2198889d250815b48
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS

diff -r 9a82999ebbd6 -r 803729c9fd4d NEWS
--- a/NEWS	Wed Apr 04 12:22:51 2012 +0200
+++ b/NEWS	Wed Apr 04 14:08:24 2012 +0200
@@ -422,7 +422,9 @@
   - Support for multisets.
 
   - Added "use_subtype" options.
- 
+  - Added "quickcheck_locale" configuration to specify how to process
+    conjectures in a locale context.
+
 * Nitpick:
   - Fixed infinite loop caused by the 'peephole_optim' option and
     affecting 'rat' and 'real'.
diff -r 9a82999ebbd6 -r 803729c9fd4d doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Apr 04 12:22:51 2012 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Apr 04 14:08:24 2012 +0200
@@ -1382,9 +1382,9 @@
     is a quotient extension theorem. Quotient extension theorems
     allow for quotienting inside container types. Given a polymorphic
     type that serves as a container, a map function defined for this
-    container  using @{command (HOL) "enriched_type"} and a relation
+    container using @{command (HOL) "enriched_type"} and a relation
     map defined for for the container type, the quotient extension
-    theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient
+    theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3
     (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems
     are stored in a database and are used all the steps of lifting
     theorems.
@@ -1740,6 +1740,15 @@
     \item[@{text no_assms}] specifies whether assumptions in
     structured proofs should be ignored.
 
+    \item[@{text locale}] specifies how to process conjectures in
+    a locale context, i.e., they can be interpreted or expanded.
+    The option is a whitespace-separated list of the two words
+    @{text interpret} and @{text expand}. The list determines the
+    order they are employed. The default setting is to first use 
+    interpretations and then test the expanded conjecture.
+    The option is only provided as attribute declaration, but not
+    as parameter to the command. 
+
     \item[@{text timeout}] sets the time limit in seconds.
 
     \item[@{text default_type}] sets the type(s) generally used to
diff -r 9a82999ebbd6 -r 803729c9fd4d doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Apr 04 12:22:51 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Apr 04 14:08:24 2012 +0200
@@ -1959,9 +1959,9 @@
     is a quotient extension theorem. Quotient extension theorems
     allow for quotienting inside container types. Given a polymorphic
     type that serves as a container, a map function defined for this
-    container  using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
+    container using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
     map defined for for the container type, the quotient extension
-    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
+    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient{\isadigit{3}}\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient{\isadigit{3}}\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
     are stored in a database and are used all the steps of lifting
     theorems.
 
@@ -2504,6 +2504,15 @@
     \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in
     structured proofs should be ignored.
 
+    \item[\isa{locale}] specifies how to process conjectures in
+    a locale context, i.e., they can be interpreted or expanded.
+    The option is a whitespace-separated list of the two words
+    \isa{interpret} and \isa{expand}. The list determines the
+    order they are employed. The default setting is to first use 
+    interpretations and then test the expanded conjecture.
+    The option is only provided as attribute declaration, but not
+    as parameter to the command. 
+
     \item[\isa{timeout}] sets the time limit in seconds.
 
     \item[\isa{default{\isaliteral{5F}{\isacharunderscore}}type}] sets the type(s) generally used to