# HG changeset patch
# User bulwahn
# Date 1327392804 -3600
# Node ID ecda235288334e51f4f3ddb8ff432891d9b7f0a4
# Parent  9a5d8e7684e552d164ffa987b3e974baa1d0385a
adding some rules to quickcheck's preprocessing

diff -r 9a5d8e7684e5 -r ecda23528833 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Jan 24 09:12:29 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Jan 24 09:13:24 2012 +0100
@@ -262,7 +262,8 @@
     val thy = Proof_Context.theory_of ctxt
     val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
     val rewrs = map (swap o dest) @{thms all_simps} @
-      (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}])
+      (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
+        @{thm bot_fun_def}, @{thm less_bool_def}])
     val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
     val (vs, body) = strip_all t'
     val vs' = Variable.variant_frees ctxt [t'] vs