equal
deleted
inserted
replaced
129 end; |
129 end; |
130 |
130 |
131 (*Default action is to print an error message; could be suppressed for |
131 (*Default action is to print an error message; could be suppressed for |
132 special applications.*) |
132 special applications.*) |
133 fun result_error_default state msg : thm = |
133 fun result_error_default state msg : thm = |
134 (writeln "Bad final proof state:"; |
134 Pretty.str "Bad final proof state:" :: pretty_goals (!goals_limit) state @ |
135 print_goals (!goals_limit) state; |
135 [Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error; |
136 writeln msg; error "Proof failed"); |
|
137 |
136 |
138 val result_error_fn = ref result_error_default; |
137 val result_error_fn = ref result_error_default; |
139 |
138 |
140 (* alternative to standard: this function does not discharge the hypotheses |
139 (* alternative to standard: this function does not discharge the hypotheses |
141 first. Is used for locales, in the following function prepare_proof *) |
140 first. Is used for locales, in the following function prepare_proof *) |