| changeset 69913 | ca515cf61651 |
| parent 69906 | 55534affe445 |
| child 69914 | 72301e1457b9 |
--- a/NEWS Thu Mar 14 16:35:58 2019 +0100 +++ b/NEWS Thu Mar 14 16:55:06 2019 +0100 @@ -40,6 +40,10 @@ need to provide a closed expression -- without trailing semicolon. Minor INCOMPATIBILITY. +* Command keywords of kind thy_decl / thy_goal may be more specifically +fit into the traditional document model of "definition-statement-proof" +via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. + *** Isabelle/jEdit Prover IDE ***