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>

licenses: convert license tags to SPDX

global: isabelle update_cartouches

aspec: Update ASpec for GrantReply (SELFOUR-6)

aspec: message_info_to_data is mostly arch independent

Factored out msg_label_bits, which is the only architecture specific part.

spec: add SetTLSBase invocation and update the registers (VER-807)

SELFOUR-1016: fix confused deputy problem when setting priorities

Removes all trailing whitespaces

SELFOUR-64: Remove general Recycle operation

This removes the RecycleCap CNodeInvocation, whilst
retaining recycle behaviour for Endpoints -- now renamed
CNodeCancelBadgedSends.

SELFOUR-444: Abstract implementation.

Abstract implementation of preemptible retyping.

SELFOUR-276: Finish proofs for maximum controlled priority (MCP)

To finish the proof of refinement to C, the specification for checkPrio
needed strengthening: the checkPrio spec now takes a machine word
argument. In the spec, priorities are still stored as 8-bit quantities,
however. Once the spec was strenthened, it was possible to remove some
redundant checks and mask operations from the C code.

A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).

SELFOUR-276: Add MCP to specs and invariants

A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).

SELFOUR-421: first attempt at abstract spec

arch_split: invariants: split Ipc_AI [VER-572]

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.

arch_split: added ARM_A and ARM_H locales

arch_split: More namespacing progress and invariant splitting. Checks halfway into Invariants_AI

arch_split: progress on namespacing abstract spec

msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API

archirq: Remove redundant invocation, renamed
arch_decode_interrupt_control.

paramatrised abstract and haskell specs over L4V_ARCH

Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.

add arch_tcb object to C, rename aep -> ntfn

history squashed patch for aep-binding

fewer warnings

ioapic: first abstract spec

Import release snapshot.