equal
deleted
inserted
replaced
39 () |
39 () |
40 *} |
40 *} |
41 |
41 |
42 ML {* |
42 ML {* |
43 if do_it then |
43 if do_it then |
44 evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir) |
44 evaluate_mash_suggestions @{context} params (1, NONE) |
45 (prefix ^ "mash_suggestions") (prefix ^ "mash_prover_suggestions") |
45 [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN] |
46 (prefix ^ "mash_eval") |
46 (SOME prob_dir) (prefix ^ "mash_suggestions") |
|
47 (prefix ^ "mash_prover_suggestions") (prefix ^ "mash_eval") |
47 else |
48 else |
48 () |
49 () |
49 *} |
50 *} |
50 |
51 |
51 end |
52 end |