# HG changeset patch
# User wenzelm
# Date 1394623121 -3600
# Node ID cd9ce893f2d6fc2063c64a9a2125b94f90556a01
# Parent  c6a15aa64e36c0ae153aa650eb2458fa3b56d41a# Parent  ad6bd8030d88efdfd3cd55280dcc8fb363a9d8b2
merged

diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Main.thy	Wed Mar 12 12:18:41 2014 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
 begin
 
 text {*
diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Wed Mar 12 12:18:41 2014 +0100
@@ -263,10 +263,9 @@
 subsection {* Measurability for (co)inductive predicates *}
 
 lemma measurable_lfp:
-  assumes "P = lfp F"
   assumes "Order_Continuity.continuous F"
   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
-  shows "pred M P"
+  shows "pred M (lfp F)"
 proof -
   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. False) x)"
       by (induct i) (auto intro!: *) }
@@ -274,16 +273,15 @@
     by measurable
   also have "(\<lambda>x. \<exists>i. (F ^^ i) (\<lambda>x. False) x) = (SUP i. (F ^^ i) bot)"
     by (auto simp add: bot_fun_def)
-  also have "\<dots> = P"
-    unfolding `P = lfp F` by (rule continuous_lfp[symmetric]) fact
+  also have "\<dots> = lfp F"
+    by (rule continuous_lfp[symmetric]) fact
   finally show ?thesis .
 qed
 
 lemma measurable_gfp:
-  assumes "P = gfp F"
   assumes "Order_Continuity.down_continuous F"
   assumes *: "\<And>A. pred M A \<Longrightarrow> pred M (F A)"
-  shows "pred M P"
+  shows "pred M (gfp F)"
 proof -
   { fix i have "Measurable.pred M (\<lambda>x. (F ^^ i) (\<lambda>x. True) x)"
       by (induct i) (auto intro!: *) }
@@ -291,8 +289,8 @@
     by measurable
   also have "(\<lambda>x. \<forall>i. (F ^^ i) (\<lambda>x. True) x) = (INF i. (F ^^ i) top)"
     by (auto simp add: top_fun_def)
-  also have "\<dots> = P"
-    unfolding `P = gfp F` by (rule down_continuous_gfp[symmetric]) fact
+  also have "\<dots> = gfp F"
+    by (rule down_continuous_gfp[symmetric]) fact
   finally show ?thesis .
 qed
 
diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Mar 12 12:18:41 2014 +0100
@@ -3,7 +3,7 @@
 header {* Counterexample generator performing narrowing-based testing *}
 
 theory Quickcheck_Narrowing
-imports Quickcheck_Exhaustive
+imports Quickcheck_Random
 keywords "find_unused_assms" :: diag
 begin
 
diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Record.thy	Wed Mar 12 12:18:41 2014 +0100
@@ -9,7 +9,7 @@
 header {* Extensible records with structural subtyping *}
 
 theory Record
-imports Quickcheck_Narrowing
+imports Quickcheck_Exhaustive
 keywords "record" :: thy_decl
 begin
 
diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/SMT.thy	Wed Mar 12 12:18:41 2014 +0100
@@ -425,7 +425,6 @@
   by auto
 
 
-
 hide_type (open) pattern
 hide_const Pattern fun_app term_true term_false z3div z3mod
 hide_const (open) trigger pat nopat weight
diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Wed Mar 12 12:18:41 2014 +0100
@@ -5,7 +5,7 @@
 header {* Word examples for for SMT binding *}
 
 theory SMT_Word_Examples
-imports Word
+imports "~~/src/HOL/Word/Word"
 begin
 
 declare [[smt_oracle = true]]
diff -r ad6bd8030d88 -r cd9ce893f2d6 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Mar 12 10:42:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Mar 12 12:18:41 2014 +0100
@@ -1222,7 +1222,7 @@
                 fold_thms lthy ctr_defs'
                   (unfold_thms lthy (pre_rel_def :: abs_inverse ::
                        (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
-                       @{thms vimage2p_def Inl_Inr_False})
+                       @{thms vimage2p_def sum.inject Inl_Inr_False})
                      (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
                 |> postproc
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);