History log of /seL4-l4v-master/l4v/lib/RangeMap.thy
Revision Date Author Comments
# 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


# c397b16f 19-May-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib: license header for RangeMap


# 071ebbd3 16-Apr-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib: move @{mk_term} antiquotation from AutoCorres; add examples


# c96444b7 16-Apr-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib/RangeMap: cleanup; strengthen range lookup thms; add testsuite


# 4f1c452b 13-Mar-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib: add RangeMap data structure (no tests yet)