equal
deleted
inserted
replaced
93 fun import_theorem ctxt thm = if is_too_generic thm then [] else |
93 fun import_theorem ctxt thm = if is_too_generic thm then [] else |
94 [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt); |
94 [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt); |
95 |
95 |
96 fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt; |
96 fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt; |
97 |
97 |
98 fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f |
98 fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f |
99 |
99 |
100 fun nth_hol_goal thm i = |
100 fun nth_hol_goal thm i = |
101 HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1)))) |
101 HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1)))) |
102 |
102 |
103 fun dest_measurable_fun t = |
103 fun dest_measurable_fun t = |