equal
deleted
inserted
replaced
680 val conjecture_shape = |
680 val conjecture_shape = |
681 conjecture_offset + 1 |
681 conjecture_offset + 1 |
682 upto conjecture_offset + length hyp_ts + 1 |
682 upto conjecture_offset + length hyp_ts + 1 |
683 |> map single |
683 |> map single |
684 val ((output, msecs), (atp_proof, outcome)) = |
684 val ((output, msecs), (atp_proof, outcome)) = |
685 TimeLimit.timeLimit generous_slice_timeout bash_output command |
685 TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command |
686 |>> (if overlord then |
686 |>> (if overlord then |
687 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
687 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
688 else |
688 else |
689 I) |
689 I) |
690 |> fst |
690 |> fst |