# HG changeset patch
# User bulwahn
# Date 1327328582 -3600
# Node ID 1c9a548c0402149a26983210c7b30768ed3a5df6
# Parent  40522961d4b11df5beb33dd1bf263daeeabd52d3
support for Ex1 in quickcheck-narrowing

diff -r 40522961d4b1 -r 1c9a548c0402 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jan 23 15:22:33 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jan 23 15:23:02 2012 +0100
@@ -388,7 +388,8 @@
     map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
       (@{thms all_simps} @ @{thms ex_simps})
     @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
-        [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}]
+        [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
+         @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
 
 fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t