src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Fri Sep 10 23:56:35 2010 +0200
+++ b/src/HOL/SMT.thy	Mon Sep 13 06:02:47 2010 +0200
@@ -241,6 +241,13 @@
 
 declare [[ z3_options = "" ]]
 
+text {*
+The following configuration option may be used to enable mapping of
+HOL datatypes and records to native datatypes provided by Z3.
+*}
+
+declare [[ z3_datatypes = false ]]
+
 
 
 subsection {* Schematic rules for Z3 proof reconstruction *}