History log of /seL4-l4v-master/l4v/camkes/glue-spec/example-dataport/GenDataportBase.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


# c34840d0 05-Jun-2019 Gerwin Klein <gerwin.klein@data61.csiro.au>

global: isabelle update_cartouches


# 0b039a07 24-Oct-2016 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Isabelle2016-1: syntax: use semantic markup instead of "header"


# a50574d3 14-Sep-2014 David Greenaway <david.greenaway@nicta.com.au>

camkes: Port to Isabelle 2014.

The only major change is that "embed" is now a constant in HOL, removing
it from the set of valid names for free variables.

Have renamed uses of "embed" to "embed_data"; a better name could
probably be chosen by someone more familiar with the code.


# 2a03e81d 14-Jul-2014 Gerwin Klein <gerwin.klein@nicta.com.au>

Import release snapshot.