equal
deleted
inserted
replaced
37 val prover = hd provers |
37 val prover = hd provers |
38 val slack_max_facts = max_facts_slack * the max_facts |
38 val slack_max_facts = max_facts_slack * the max_facts |
39 val path = file_name |> Path.explode |
39 val path = file_name |> Path.explode |
40 val lines = path |> File.read_lines |
40 val lines = path |> File.read_lines |
41 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
41 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
42 val facts = all_facts_of thy css_table |
42 val facts = all_facts_of (Proof_Context.init_global thy) css_table |
43 val all_names = all_names (facts |> map snd) |
43 val all_names = all_names (facts |> map snd) |
44 val mepo_ok = Unsynchronized.ref 0 |
44 val mepo_ok = Unsynchronized.ref 0 |
45 val mash_ok = Unsynchronized.ref 0 |
45 val mash_ok = Unsynchronized.ref 0 |
46 val mesh_ok = Unsynchronized.ref 0 |
46 val mesh_ok = Unsynchronized.ref 0 |
47 val isar_ok = Unsynchronized.ref 0 |
47 val isar_ok = Unsynchronized.ref 0 |