--- a/src/HOL/Probability/measurable.ML Fri Aug 16 21:28:05 2013 +0200
+++ b/src/HOL/Probability/measurable.ML Fri Aug 16 21:33:36 2013 +0200
@@ -8,13 +8,13 @@
sig
datatype level = Concrete | Generic
- val simproc : Proof.context -> cterm -> thm option
- val method : (Proof.context -> Method.method) context_parser
+ 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 measurable_tac : Proof.context -> thm list -> tactic
- val attr : attribute context_parser
- val dest_attr : attribute context_parser
- val app_attr : attribute context_parser
+ val simproc : Proof.context -> cterm -> thm option
val get : level -> Proof.context -> thm list
val get_all : Proof.context -> thm list
@@ -213,21 +213,6 @@
fun measurable_tac ctxt facts =
TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
-val attr_add = Thm.declaration_attribute o add_thm;
-
-val attr : attribute context_parser =
- Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
- Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
-
-val dest_attr : attribute context_parser =
- Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
-
-val app_attr : attribute context_parser =
- Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
-
-val method : (Proof.context -> Method.method) context_parser =
- Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
-
fun simproc ctxt redex =
let
val t = HOLogic.mk_Trueprop (term_of redex);