equal
deleted
inserted
replaced
9 (in ../lib/Tools/mirabelle) with the parameters actually used by this |
9 (in ../lib/Tools/mirabelle) with the parameters actually used by this |
10 interface, the former extracts PARAMETER and DESCRIPTION from code below which |
10 interface, the former extracts PARAMETER and DESCRIPTION from code below which |
11 has this pattern (provided it appears in a single line): |
11 has this pattern (provided it appears in a single line): |
12 val .*K = "PARAMETER" (*DESCRIPTION*) |
12 val .*K = "PARAMETER" (*DESCRIPTION*) |
13 *) |
13 *) |
|
14 (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) |
14 |
15 |
15 val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) |
16 val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) |
16 val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) |
17 val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) |
17 val fact_filterK = "fact_filter" (*=STRING: fact filter*) |
18 val fact_filterK = "fact_filter" (*=STRING: fact filter*) |
18 val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) |
19 val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) |