# HG changeset patch
# User Andreas Lochbihler
# Date 1415692666 -3600
# Node ID a62cdcc5344b02a7e6acc0096b5ed98874d19348
# Parent  a93d114eaa5d96fbd15c94a1f065b3a6ab5bd54a
add del option to measurable;
make measurability rules available as dynamic theorem;

diff -r a93d114eaa5d -r a62cdcc5344b src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Tue Nov 11 00:11:11 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Tue Nov 11 08:57:46 2014 +0100
@@ -51,9 +51,10 @@
 ML_file "measurable.ML"
 
 attribute_setup measurable = {*
-  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
-    Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
-    (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm))
+  Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true --
+    Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+      Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
+    (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm))
 *} "declaration of measurability theorems"
 
 attribute_setup measurable_dest = {*
@@ -70,6 +71,10 @@
 
 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
 
+setup {*
+  Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of)
+*}
+
 declare
   measurable_compose_rev[measurable_dest]
   pred_sets1[measurable_dest]
diff -r a93d114eaa5d -r a62cdcc5344b src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Tue Nov 11 00:11:11 2014 +0100
+++ b/src/HOL/Probability/measurable.ML	Tue Nov 11 08:57:46 2014 +0100
@@ -11,6 +11,8 @@
   val add_app : thm -> Context.generic -> Context.generic
   val add_dest : thm -> Context.generic -> Context.generic
   val add_thm : bool * level -> thm -> Context.generic -> Context.generic
+  val del_thm : bool * level -> thm -> Context.generic -> Context.generic
+  val add_del_thm : bool -> (bool * level) -> thm -> Context.generic -> Context.generic
 
   val measurable_tac : Proof.context -> thm list -> tactic
 
@@ -20,7 +22,6 @@
   val get_all : Proof.context -> thm list
 
   val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
-
 end ;
 
 structure Measurable : MEASURABLE =
@@ -77,6 +78,7 @@
 
 fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
 fun add thms' = update (fold Item_Net.update thms');
+fun del thms' = update (fold Item_Net.remove thms');
 
 val get_dest = Item_Net.content o #dest_thms o Data.get;
 val add_dest = Data.map o map_dest_thms o Item_Net.update;
@@ -93,7 +95,12 @@
 fun import_theorem ctxt thm = if is_too_generic thm then [] else
   [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
 
-fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
+fun add_del_thm_gen f (raw, lv) thm ctxt = f (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
+
+val add_thm = add_del_thm_gen add;
+val del_thm = add_del_thm_gen del;
+fun add_del_thm true = add_thm
+  | add_del_thm false = del_thm
 
 fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f