equal
deleted
inserted
replaced
333 platforms (Cygwin). Provers are no longer hardwired, but defined |
333 platforms (Cygwin). Provers are no longer hardwired, but defined |
334 within the theory via plain ML wrapper functions. Basic Sledgehammer |
334 within the theory via plain ML wrapper functions. Basic Sledgehammer |
335 commands are covered in the isar-ref manual. |
335 commands are covered in the isar-ref manual. |
336 |
336 |
337 * Wrapper scripts for remote SystemOnTPTP service allows to use |
337 * Wrapper scripts for remote SystemOnTPTP service allows to use |
338 sledgehammer without local ATP installation (Vampire etc.). See also |
338 sledgehammer without local ATP installation (Vampire etc.). Other |
339 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
339 provers may be included via suitable ML wrappers, see also |
340 variable. Other provers may be included via suitable ML wrappers, see |
340 src/HOL/ATP_Linkup.thy. |
341 also src/HOL/ATP_Linkup.thy. |
|
342 |
341 |
343 * Normalization by evaluation now allows non-leftlinear equations. |
342 * Normalization by evaluation now allows non-leftlinear equations. |
344 Declare with attribute [code nbe]. |
343 Declare with attribute [code nbe]. |
345 |
344 |
346 * Command "value" now integrates different evaluation |
345 * Command "value" now integrates different evaluation |