equal
deleted
inserted
replaced
63 demanding keyword 'by' and supporting the full method expression |
63 demanding keyword 'by' and supporting the full method expression |
64 syntax just like the Isar command 'by'. |
64 syntax just like the Isar command 'by'. |
65 |
65 |
66 |
66 |
67 *** HOL *** |
67 *** HOL *** |
|
68 |
|
69 * Wrapper script for remote SystemOnTPTP service allows to use |
|
70 sledghammer without local ATP installation (Vampire etc.); see |
|
71 ISABELLE_HOME/contrib/SystemOnTPTP/. |
68 |
72 |
69 * Normalization by evaluation now allows non-leftlinear equations. |
73 * Normalization by evaluation now allows non-leftlinear equations. |
70 Declare with attribute [code nbe]. |
74 Declare with attribute [code nbe]. |
71 |
75 |
72 * Command "value" now integrates different evaluation |
76 * Command "value" now integrates different evaluation |