equal
deleted
inserted
replaced
250 Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => |
250 Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => |
251 let |
251 let |
252 val f = dest_measurable_fun (HOLogic.dest_Trueprop t) |
252 val f = dest_measurable_fun (HOLogic.dest_Trueprop t) |
253 fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt))) |
253 fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt))) |
254 fun inst (ts, Ts) = |
254 fun inst (ts, Ts) = |
255 Drule.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts) |
255 Thm.instantiate' (cert Thm.global_ctyp_of Ts) (cert Thm.global_cterm_of ts) |
256 @{thm measurable_compose_countable} |
256 @{thm measurable_compose_countable} |
257 in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end |
257 in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end |
258 handle TERM _ => no_tac) 1) |
258 handle TERM _ => no_tac) 1) |
259 |
259 |
260 val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac |
260 val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac |