History log of /seL4-l4v-master/l4v/tools/asmrefine/CommonOpsLemmas.thy
Revision Date Author Comments
# a424d55e 09-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX


# c1747628 17-Dec-2019 Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>

asmrefine: Add support for 64-bit architectures.


# b5cdf470 13-Jun-2018 Gerwin Klein <gerwin.klein@data61.csiro.au>

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.


# 41d4aa4f 25-Oct-2016 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Isabelle2016-1: update references to renamed constants and facts


# 93adccc1 30-May-2016 Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au>

license-tool: missing license headers + .licenseignore [VER-551]


# f52bc138 19-May-2016 Joel Beeren <joel.beeren@nicta.com.au>

lib: fix theory includes for arch-splitted WordSetup


# 6a2692ab 19-May-2016 Joel Beeren <joel.beeren@nicta.com.au>

lib: fix theory includes for arch-splitted WordSetup


# 322f1023 18-Apr-2016 Gerwin Klein <gerwin.klein@nicta.com.au>

word_lib: adjust theory dependencies


# 175eb2da 02-Dec-2015 Thomas Sewell <Thomas.Sewell@nicta.com.au>

More fixes for pointer array assertions.


# df404257 02-Dec-2015 Thomas Sewell <Thomas.Sewell@nicta.com.au>

Repair SimplExport/GraphRefine.


# ca439188 21-May-2015 Thomas Sewell <Thomas.Sewell@nicta.com.au>

WIP on WCET annotations.