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

licenses: convert license tags to SPDX


# 0d3325ee 25-Aug-2017 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

Isabelle2017: update lib for RC0

* ML Proof_Context.fact_alias renamed to alias_fact.

* Named_Target.init removed redundant parameter.

* Simplified Greatest, removed GreatestM.

* Introduced thm_node type in proofterm.ML.


# 796887d9 11-Jul-2017 Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au>

Removes all trailing whitespaces


# 60afdc12 08-May-2016 Matthew Brecknell <Matthew.Brecknell@nicta.com.au>

trivial: fixups including some licence headers


# 670d1c11 02-May-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: added optional definition override for crunch. Reduced qualification commands to minimal required set.


# 1d20b393 26-Apr-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: replaced sublocale with global_naming


# 18a381bd 30-Mar-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: fix for qualification issue with duplicate consts. Needs to be tested on ASpec/AInvs still.


# d0a29887 23-Mar-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: checkpoint for namespacing haskell


# df8261c1 16-Feb-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: split up Invariants_AI


# 1018d01b 04-Feb-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

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


# 9718f1bd 04-Feb-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: progress on namespacing abstract spec