adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

readme: use -R instead of -l 

Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
This commit is contained in:
Corey Lewis 2021-01-08 13:51:09 +11:00 committed by Corey Lewis
parent 752014b466
commit be9175c5bf
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
README.md
View File

@ -191,10 +191,10 @@ from the directory `l4v/`. For available sessions, see the corresponding
each major directory in the repository.
For interactively exploring, say the invariant proof of the abstract
specification with a pre-built logic image for the abstract specification,
run
specification with a pre-built logic image for the abstract specification and
all of the invariant proof's dependencies, run
./isabelle/bin/isabelle jedit -d . -l ASpec
./isabelle/bin/isabelle jedit -d . -R AInvs
in `l4v/` and open one of the files in `proof/invariant-abstract`.