..
ADT_H.thy
SELFOUR-421: infoflow and infoflow_c builds
2016-09-22 19:11:37 +10:00
ArchAcc_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
Arch_R.thy
SELFOUR-421: infoflow and infoflow_c builds
2016-09-22 19:11:37 +10:00
Bits_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
BuildRefineCache.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
CNodeInv_R.thy
SELFOUR-421: refine done
2016-09-22 19:11:36 +10:00
CSpace1_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
CSpace_I.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
CSpace_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
Cache.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Corres.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Detype_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
EmptyFail.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
EmptyFail_H.thy
SELFOUR-56: Remove diminish rights from IPC
2016-02-24 13:24:10 +11:00
Finalise_R.thy
SELFOUR-421: infoflow and infoflow_c builds
2016-09-22 19:11:37 +10:00
IncKernelInit.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
Include.thy
repair ARM proofs up to Refine after factoring out architecture
2016-01-13 12:02:12 +11:00
InitLemmas.thy
2015 update for Refine
2015-05-12 17:17:31 +02:00
InterruptAcc_R.thy
add arch_tcb object to C, rename aep -> ntfn
2015-11-20 16:02:13 +11:00
Interrupt_R.thy
l4v-sabre: move a few word lemmas to WordLemmaBucket and fix styles of some proofs
2016-02-17 11:18:03 +11:00
Invariants_H.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
Invocations_R.thy
Import release snapshot.
2014-07-14 21:32:44 +02:00
IpcCancel_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
Ipc_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
KHeap_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
KernelInit_R.thy
abstract Haskell init parameters into constants
2014-11-06 18:48:36 +11:00
LevityCatch.thy
add arch_tcb object to C, rename aep -> ntfn
2015-11-20 16:02:13 +11:00
Machine_R.thy
l4v-sabre: change type of irq to be 10 word
2016-02-17 11:18:02 +11:00
Orphanage.thy
SELFOUR-421: fix refine
2016-09-22 19:11:36 +10:00
PageTableDuplicates.thy
SELFOUR-421: fix refine
2016-09-22 19:11:36 +10:00
RAB_FN.thy
Finally done with array assertions.
2015-12-02 09:08:27 +11:00
README.md
misc: Proofing and formatting of README.md files.
2014-07-28 13:15:48 +10:00
Refine.thy
SELFOUR-421: infoflow and infoflow_c builds
2016-09-22 19:11:37 +10:00
Retype_R.thy
SELFOUR-421: infoflow and infoflow_c builds
2016-09-22 19:11:37 +10:00
Schedule_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
StateRelation.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
SubMonad_R.thy
2015 update for Refine
2015-05-12 17:17:31 +02:00
Syscall_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
TcbAcc_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
Tcb_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00
Untyped_R.thy
SELFOUR-421: infoflow and infoflow_c builds
2016-09-22 19:11:37 +10:00
VSpace_R.thy
SELFOUR-421: crefine builds
2016-09-22 19:11:37 +10:00