equal
deleted
inserted
replaced
63 string Symtab.table * string Symtab.table -> thm -> string list |
63 string Symtab.table * string Symtab.table -> thm -> string list |
64 val prover_dependencies_of : |
64 val prover_dependencies_of : |
65 Proof.context -> params -> string -> int -> fact list |
65 Proof.context -> params -> string -> int -> fact list |
66 -> string Symtab.table * string Symtab.table -> thm |
66 -> string Symtab.table * string Symtab.table -> thm |
67 -> bool * string list |
67 -> bool * string list |
|
68 val weight_mepo_facts : 'a list -> ('a * real) list |
68 val weight_mash_facts : 'a list -> ('a * real) list |
69 val weight_mash_facts : 'a list -> ('a * real) list |
69 val find_mash_suggestions : |
70 val find_mash_suggestions : |
70 int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list |
71 int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list |
71 -> ('b * thm) list * ('b * thm) list |
72 -> ('b * thm) list * ('b * thm) list |
72 val mash_suggested_facts : |
73 val mash_suggested_facts : |
756 (Graph.imm_preds access_G new) news)) |
757 (Graph.imm_preds access_G new) news)) |
757 in find_maxes Symtab.empty ([], Graph.maximals access_G) end |
758 in find_maxes Symtab.empty ([], Graph.maximals access_G) end |
758 |
759 |
759 fun is_fact_in_graph access_G get_th fact = |
760 fun is_fact_in_graph access_G get_th fact = |
760 can (Graph.get_node access_G) (nickname_of_thm (get_th fact)) |
761 can (Graph.get_node access_G) (nickname_of_thm (get_th fact)) |
|
762 |
|
763 (* FUDGE *) |
|
764 fun weight_of_mepo_fact rank = |
|
765 Math.pow (0.62, log2 (Real.fromInt (rank + 1))) |
|
766 |
|
767 fun weight_mepo_facts facts = |
|
768 facts ~~ map weight_of_mepo_fact (0 upto length facts - 1) |
761 |
769 |
762 val weight_raw_mash_facts = weight_mepo_facts |
770 val weight_raw_mash_facts = weight_mepo_facts |
763 val weight_mash_facts = weight_raw_mash_facts |
771 val weight_mash_facts = weight_raw_mash_facts |
764 |
772 |
765 (* FUDGE *) |
773 (* FUDGE *) |