344 Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode |
344 Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode |
345 Nat_Int_Bij.inj_nat_to_int_bij ~> inj_int_encode |
345 Nat_Int_Bij.inj_nat_to_int_bij ~> inj_int_encode |
346 Nat_Int_Bij.inj_int_to_nat_bij ~> inj_int_decode |
346 Nat_Int_Bij.inj_int_to_nat_bij ~> inj_int_decode |
347 Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_encode |
347 Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_encode |
348 Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode |
348 Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode |
|
349 |
|
350 * Sledgehammer: |
|
351 - Renamed ATP commands: |
|
352 atp_info ~> sledgehammer running_atps |
|
353 atp_kill ~> sledgehammer kill_atps |
|
354 atp_messages ~> sledgehammer messages |
|
355 atp_minimize ~> sledgehammer minimize |
|
356 print_atps ~> sledgehammer available_atps |
|
357 INCOMPATIBILITY. |
|
358 - Added user's manual ("isabelle doc sledgehammer"). |
|
359 - Added option syntax and "sledgehammer_params" to customize |
|
360 Sledgehammer's behavior. See the manual for details. |
|
361 - Modified the Isar proof reconstruction code so that it produces |
|
362 direct proofs rather than proofs by contradiction. (This feature |
|
363 is still experimental.) |
|
364 - Made Isar proof reconstruction work for SPASS, remote ATPs, and in |
|
365 full-typed mode. |
|
366 - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP. |
349 |
367 |
350 * Nitpick: |
368 * Nitpick: |
351 - Added and implemented "binary_ints" and "bits" options. |
369 - Added and implemented "binary_ints" and "bits" options. |
352 - Added "std" option and implemented support for nonstandard models. |
370 - Added "std" option and implemented support for nonstandard models. |
353 - Added and implemented "finitize" option to improve the precision |
371 - Added and implemented "finitize" option to improve the precision |