Commit 5d5daeba authored by MARCHE Claude's avatar MARCHE Claude

compute_in_goal as a strategy

parent 309ca235
......@@ -153,6 +153,8 @@ let default_strategies =
[|"t split_goal_wp 1"|];
"Inline", "Inline@ function@ symbols@ once", "i",
[|"t inline_goal 1"|];
"Compute", "Compute@ in@ goal", "c",
[|"t compute_in_goal 1"|];
]
let get_strategies ?(default=[]) rc =
......
......@@ -511,7 +511,7 @@ let show_legend_window () =
ib image_prover;
i " External prover\n";
ib image_transf;
i " Transformation\n";
i " Transformation or strategy\n";
it "Status column\n";
ib image_undone;
i " External proof attempt not done\n";
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment