#
a45adef6 |
|
31-Oct-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
all: remove theory import path references In Isabelle2020, when isabelle jedit is started without a session context, e.g. `isabelle jedit -l ASpec`, theory imports with path references cause the isabelle process to hang. Since sessions now declare directories, Isabelle can find those files without path reference and we therefore remove all such path references from import statements. With this, `jedit` and `build` should work with and without explicit session context as before. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
bd4392d1 |
|
07-May-2020 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
lib: add ML_goal command Sometimes we want to prove a fact, but the fact is painful or error-prone to type out manually. In these cases, we'd like to construct the goal fact using ML and then immediately enter a proof block. Previously, we could achieve something like this through careful use of `Thm.trivial` and `schematic_goal`, but this would clutter up the ML namespace and wouln't handle meta conjuncts (`&&&`). The new `ML_goal` command addresses both of these issues. Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
|