#
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
|
#
9a9c6320 |
|
17-Jul-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: various crunch improvements The main one is that crunch now uses wpsimp when determining whether a goal can already be solved, instead of just wp. Crunch can also now use wps when proving a goal and will now always ignore a constant if told to, even if it is the top-level constant being crunched.
|
#
c34840d0 |
|
05-Jun-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
global: isabelle update_cartouches
|
#
a74b7b40 |
|
11-Oct-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: clean up BCorres_UL
|
#
d77d31a7 |
|
03-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
47119bf4 |
|
13-Jan-2017 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
|
#
9a1ec71a |
|
23-Aug-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Refactor of crunch. Substantial adjustments to crunch. Main user changes are: - 'lift' and 'unfold' mechanisms replaced by more general 'rule'. - some more 'ignores' standardised. - crunch has a more principled overall design: + discover crunch rule * provided or by definition extraction + recurse according to rule + prove goal based on rule, recursive discoveries, standard tactic * wp/simp adjustments tweak tactic
|
#
84b923a6 |
|
17-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib: start disentangling spaghetti word dependencies
|
#
fc6e5771 |
|
10-Aug-2014 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Proof updates, working as far as AInvs.
|
#
50dda770 |
|
22-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
comment cleanup
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|