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