equal
deleted
inserted
replaced
59 "") ^ |
59 "") ^ |
60 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
60 " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
61 (if blocking then |
61 (if blocking then |
62 "." |
62 "." |
63 else |
63 else |
64 ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
64 "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
65 |
65 |
66 val auto_minimize_min_facts = |
66 val auto_minimize_min_facts = |
67 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
67 Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
68 (fn generic => Config.get_generic generic binary_min_facts) |
68 (fn generic => Config.get_generic generic binary_min_facts) |
69 |
69 |