equal
deleted
inserted
replaced
34 Sledgehammer_Isar.default_params ctxt [] |
34 Sledgehammer_Isar.default_params ctxt [] |
35 val prover = hd provers |
35 val prover = hd provers |
36 val slack_max_facts = max_facts_slack * the max_facts |
36 val slack_max_facts = max_facts_slack * the max_facts |
37 val path = file_name |> Path.explode |
37 val path = file_name |> Path.explode |
38 val lines = path |> File.read_lines |
38 val lines = path |> File.read_lines |
39 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
39 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
40 val facts = all_facts_of (Proof_Context.init_global thy) css_table |
40 val facts = |
|
41 all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css |
41 val all_names = all_names (facts |> map snd) |
42 val all_names = all_names (facts |> map snd) |
42 val mepo_ok = Unsynchronized.ref 0 |
43 val mepo_ok = Unsynchronized.ref 0 |
43 val mash_ok = Unsynchronized.ref 0 |
44 val mash_ok = Unsynchronized.ref 0 |
44 val mesh_ok = Unsynchronized.ref 0 |
45 val mesh_ok = Unsynchronized.ref 0 |
45 val isar_ok = Unsynchronized.ref 0 |
46 val isar_ok = Unsynchronized.ref 0 |
68 let |
69 let |
69 val (name, suggs) = extract_query line |
70 val (name, suggs) = extract_query line |
70 val th = |
71 val th = |
71 case find_first (fn (_, th) => nickname_of th = name) facts of |
72 case find_first (fn (_, th) => nickname_of th = name) facts of |
72 SOME (_, th) => th |
73 SOME (_, th) => th |
73 | NONE => error ("No fact called \"" ^ name ^ "\"") |
74 | NONE => error ("No fact called \"" ^ name ^ "\".") |
74 val goal = goal_of_thm thy th |
75 val goal = goal_of_thm thy th |
75 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
76 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
76 val isar_deps = isar_dependencies_of all_names th |> these |
77 val isar_deps = isar_dependencies_of all_names th |> these |
77 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
78 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
78 val mepo_facts = |
79 val mepo_facts = |