equal
deleted
inserted
replaced
36 val prover = hd provers |
36 val prover = hd provers |
37 val slack_max_facts = generous_max_facts (the max_facts) |
37 val slack_max_facts = generous_max_facts (the max_facts) |
38 val sugg_path = sugg_file_name |> Path.explode |
38 val sugg_path = sugg_file_name |> Path.explode |
39 val lines = sugg_path |> File.read_lines |
39 val lines = sugg_path |> File.read_lines |
40 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
40 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
41 val facts = all_facts ctxt false Symtab.empty [] [] css |
41 val facts = all_facts ctxt true false Symtab.empty [] [] css |
42 val all_names = all_names (facts |> map snd) |
42 val all_names = all_names (facts |> map snd) |
43 val mepo_ok = Unsynchronized.ref 0 |
43 val mepo_ok = Unsynchronized.ref 0 |
44 val mash_ok = Unsynchronized.ref 0 |
44 val mash_ok = Unsynchronized.ref 0 |
45 val mesh_ok = Unsynchronized.ref 0 |
45 val mesh_ok = Unsynchronized.ref 0 |
46 val isar_ok = Unsynchronized.ref 0 |
46 val isar_ok = Unsynchronized.ref 0 |