#
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>
|
#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
c34840d0 |
|
05-Jun-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
global: isabelle update_cartouches
|
#
e8e40a57 |
|
06-Jun-2019 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
lib: Use `datatype_schem` arguments in `wpfix`. `wpfix` delegates to `datatype_schem`, so we include the option to add new accessor lemmas.
|
#
1ae3a8d6 |
|
20-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: Lib update
|
#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
d4d89922 |
|
25-Feb-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib/wp: Adjust some problematic attributes. In particular, some intro! attributes for some wp rules are removed. These previously caused auto/fastforce to play a really strange role in some proofs.
|
#
a70aeda3 |
|
21-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Datatype_Schematic and WPFix. Add two new tactics/methods which can fix common painful problems with schematic variables. Method datatype_schem improves unification outcomes, by making judicious use of selectors like fst/snd/the/hd to bring variables into scope, and also using a wrapper to avoid singleton constants like True being captured needlessly by unification. Method wpfix uses strengthen machinery to instantiate rogue postcondition schematics to True and to split precondition schematics that are shared across different sites.
|