From a45adef66ad2e1809edbd190dc14f80e381d535e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 31 Oct 2020 16:30:58 +1000 Subject: [PATCH] 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 --- .../example-dataport/GenDataportBase.thy | 2 +- .../example-dataport/UserDataport.thy | 2 +- .../glue-spec/example-event/GenEventBase.thy | 2 +- camkes/glue-spec/example-event/UserEvent.thy | 2 +- .../example-procedure/GenSimpleBase.thy | 2 +- .../glue-spec/example-procedure/UserSimple.thy | 2 +- .../example-trusted/GenFilter2Base.thy | 2 +- .../glue-spec/example-trusted/UserFilter2.thy | 2 +- .../example-untrusted/GenFilterBase.thy | 2 +- .../glue-spec/example-untrusted/UserFilter.thy | 2 +- lib/Apply_Trace.thy | 2 +- lib/AutoLevity.thy | 2 +- lib/BCorres_UL.thy | 2 +- lib/Bisim_UL.thy | 2 +- lib/Corres_UL.thy | 4 ++-- lib/Crunch.thy | 4 ++-- lib/Crunch_Instances_NonDet.thy | 4 ++-- lib/Crunch_Instances_Trace.thy | 2 +- lib/Eisbach_Methods.thy | 2 +- lib/EmptyFailLib.thy | 2 +- lib/FP_Eval.thy | 2 +- lib/GenericLib.thy | 2 +- lib/HaskellLib_H.thy | 4 ++-- lib/ML_Goal_Test.thy | 2 +- lib/MonadEq.thy | 2 +- lib/Monad_WP/Datatype_Schematic.thy | 4 ++-- lib/Monad_WP/NonDetMonad.thy | 2 +- lib/Monad_WP/NonDetMonadVCG.thy | 4 ++-- lib/Monad_WP/OptionMonad.thy | 4 ++-- lib/Monad_WP/OptionMonadWP.thy | 2 +- lib/Monad_WP/TraceMonad.thy | 4 ++-- lib/Monad_WP/TraceMonadVCG.thy | 4 ++-- lib/Monad_WP/wp/Eisbach_WP.thy | 10 +++++----- lib/Monad_WP/wp/WP.thy | 8 ++++---- lib/Monad_WP/wp/WPBang.thy | 4 ++-- lib/Monad_WP/wp/WPEx.thy | 4 ++-- lib/Monad_WP/wp/WPFix.thy | 4 ++-- lib/Monad_WP/wp/WPI.thy | 6 +++--- lib/Monad_WP/wp/WPSimp.thy | 2 +- lib/Monad_WP/wp/WP_Pre.thy | 2 +- lib/MonadicRewrite.thy | 2 +- lib/NonDetMonadLemmaBucket.thy | 6 +++--- lib/RangeMap.thy | 2 +- lib/Trace_Schematic_Insts.thy | 4 ++-- lib/Word_Lib/ARM/WordSetup.thy | 4 ++-- lib/Word_Lib/ARM_HYP/WordSetup.thy | 4 ++-- lib/Word_Lib/RISCV64/WordSetup.thy | 4 ++-- lib/Word_Lib/X64/WordSetup.thy | 4 ++-- .../examples/Peterson_Atomicity.thy | 2 +- lib/concurrency/examples/Plus2_Prefix.thy | 2 +- lib/sep_algebra/ex/Sep_Tactics_Test.thy | 2 +- .../ex/Simple_Separation_Example.thy | 4 ++-- lib/sep_algebra/ex/VM_Example.thy | 4 ++-- .../ex/capDL/Abstract_Separation_D.thy | 4 ++-- proof/crefine/ARM/ArchMove_C.thy | 2 +- proof/crefine/ARM/Ctac_lemmas_C.thy | 2 +- proof/crefine/ARM/Refine_C.thy | 2 +- proof/crefine/ARM_HYP/ArchMove_C.thy | 2 +- proof/crefine/ARM_HYP/Ctac_lemmas_C.thy | 2 +- proof/crefine/ARM_HYP/Refine_C.thy | 2 +- proof/crefine/RISCV64/ArchMove_C.thy | 2 +- proof/crefine/RISCV64/Ctac_lemmas_C.thy | 2 +- proof/crefine/RISCV64/Refine_C.thy | 2 +- proof/crefine/X64/ArchMove_C.thy | 2 +- proof/crefine/X64/Ctac_lemmas_C.thy | 2 +- proof/crefine/X64/Refine_C.thy | 2 +- proof/crefine/lib/Corres_C.thy | 2 +- proof/invariant-abstract/ADT_AI.thy | 2 +- proof/invariant-abstract/AInvs.thy | 2 +- proof/invariant-abstract/AInvsPre.thy | 2 +- proof/invariant-abstract/ARM/ArchADT_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchAInvsPre.thy | 2 +- proof/invariant-abstract/ARM/ArchAcc_AI.thy | 5 +++-- proof/invariant-abstract/ARM/ArchArch_AI.thy | 2 +- .../invariant-abstract/ARM/ArchBCorres2_AI.thy | 2 +- .../invariant-abstract/ARM/ArchBCorres_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchBits_AI.thy | 2 +- .../invariant-abstract/ARM/ArchCNodeInv_AI.thy | 2 +- .../ARM/ArchCSpaceInvPre_AI.thy | 2 +- .../ARM/ArchCSpaceInv_AI.thy | 2 +- .../ARM/ArchCSpacePre_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchCSpace_AI.thy | 2 +- .../ARM/ArchDetSchedAux_AI.thy | 2 +- .../ARM/ArchDetSchedDomainTime_AI.thy | 2 +- .../ARM/ArchDetSchedSchedule_AI.thy | 2 +- .../ARM/ArchDeterministic_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchDetype_AI.thy | 2 +- .../ARM/ArchEmptyFail_AI.thy | 2 +- .../invariant-abstract/ARM/ArchFinalise_AI.thy | 2 +- .../ARM/ArchInterruptAcc_AI.thy | 2 +- .../ARM/ArchInterrupt_AI.thy | 2 +- .../ARM/ArchInvariants_AI.thy | 2 +- .../ARM/ArchIpcCancel_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchIpc_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchKHeap_AI.thy | 2 +- .../ARM/ArchKernelInit_AI.thy | 6 +++--- proof/invariant-abstract/ARM/ArchRetype_AI.thy | 2 +- .../invariant-abstract/ARM/ArchSchedule_AI.thy | 2 +- .../invariant-abstract/ARM/ArchSyscall_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchTcbAcc_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchTcb_AI.thy | 2 +- .../invariant-abstract/ARM/ArchUntyped_AI.thy | 2 +- .../ARM/ArchVSpaceEntries_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchVSpace_AI.thy | 2 +- proof/invariant-abstract/ARM/Machine_AI.thy | 2 +- .../invariant-abstract/ARM_HYP/ArchADT_AI.thy | 2 +- .../ARM_HYP/ArchAInvsPre.thy | 2 +- .../invariant-abstract/ARM_HYP/ArchAcc_AI.thy | 5 +++-- .../invariant-abstract/ARM_HYP/ArchArch_AI.thy | 2 +- .../ARM_HYP/ArchBCorres2_AI.thy | 2 +- .../ARM_HYP/ArchBCorres_AI.thy | 2 +- .../invariant-abstract/ARM_HYP/ArchBits_AI.thy | 2 +- .../ARM_HYP/ArchCNodeInv_AI.thy | 2 +- .../ARM_HYP/ArchCSpaceInvPre_AI.thy | 2 +- .../ARM_HYP/ArchCSpaceInv_AI.thy | 2 +- .../ARM_HYP/ArchCSpacePre_AI.thy | 2 +- .../ARM_HYP/ArchCSpace_AI.thy | 2 +- .../ARM_HYP/ArchDetSchedAux_AI.thy | 2 +- .../ARM_HYP/ArchDetSchedDomainTime_AI.thy | 2 +- .../ARM_HYP/ArchDetSchedSchedule_AI.thy | 2 +- .../ARM_HYP/ArchDeterministic_AI.thy | 2 +- .../ARM_HYP/ArchDetype_AI.thy | 2 +- .../ARM_HYP/ArchEmptyFail_AI.thy | 2 +- .../ARM_HYP/ArchFinalise_AI.thy | 2 +- .../ARM_HYP/ArchInterruptAcc_AI.thy | 2 +- .../ARM_HYP/ArchInterrupt_AI.thy | 2 +- .../ARM_HYP/ArchInvariants_AI.thy | 2 +- .../ARM_HYP/ArchIpcCancel_AI.thy | 2 +- .../invariant-abstract/ARM_HYP/ArchIpc_AI.thy | 2 +- .../ARM_HYP/ArchKHeap_AI.thy | 2 +- .../ARM_HYP/ArchKernelInit_AI.thy | 6 +++--- .../ARM_HYP/ArchRetype_AI.thy | 2 +- .../ARM_HYP/ArchSchedule_AI.thy | 2 +- .../ARM_HYP/ArchSyscall_AI.thy | 2 +- .../ARM_HYP/ArchTcbAcc_AI.thy | 2 +- .../invariant-abstract/ARM_HYP/ArchTcb_AI.thy | 2 +- .../ARM_HYP/ArchUntyped_AI.thy | 2 +- .../ARM_HYP/ArchVSpaceEntries_AI.thy | 2 +- .../ARM_HYP/ArchVSpace_AI.thy | 2 +- .../invariant-abstract/ARM_HYP/Machine_AI.thy | 2 +- proof/invariant-abstract/Arch_AI.thy | 2 +- proof/invariant-abstract/BCorres2_AI.thy | 2 +- proof/invariant-abstract/Bits_AI.thy | 2 +- proof/invariant-abstract/CNodeInv_AI.thy | 2 +- proof/invariant-abstract/CSpaceInvPre_AI.thy | 2 +- proof/invariant-abstract/CSpaceInv_AI.thy | 2 +- proof/invariant-abstract/CSpacePre_AI.thy | 2 +- proof/invariant-abstract/CSpace_AI.thy | 2 +- .../DetSchedDomainTime_AI.thy | 2 +- proof/invariant-abstract/DetSchedInvs_AI.thy | 2 +- .../invariant-abstract/DetSchedSchedule_AI.thy | 2 +- proof/invariant-abstract/Detype_AI.thy | 2 +- proof/invariant-abstract/EmptyFail_AI.thy | 2 +- proof/invariant-abstract/Finalise_AI.thy | 6 +++--- proof/invariant-abstract/Include_AI.thy | 2 +- proof/invariant-abstract/InterruptAcc_AI.thy | 2 +- proof/invariant-abstract/Interrupt_AI.thy | 2 +- proof/invariant-abstract/Invariants_AI.thy | 2 +- proof/invariant-abstract/IpcCancel_AI.thy | 2 +- proof/invariant-abstract/Ipc_AI.thy | 3 ++- proof/invariant-abstract/KHeapPre_AI.thy | 2 +- proof/invariant-abstract/KHeap_AI.thy | 2 +- proof/invariant-abstract/KernelInit_AI.thy | 2 +- proof/invariant-abstract/LevityCatch_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchADT_AI.thy | 2 +- .../RISCV64/ArchAInvsPre.thy | 2 +- .../invariant-abstract/RISCV64/ArchAcc_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchArch_AI.thy | 2 +- .../RISCV64/ArchBCorres2_AI.thy | 2 +- .../RISCV64/ArchBCorres_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchBits_AI.thy | 2 +- .../RISCV64/ArchCNodeInv_AI.thy | 2 +- .../RISCV64/ArchCSpaceInvPre_AI.thy | 2 +- .../RISCV64/ArchCSpaceInv_AI.thy | 2 +- .../RISCV64/ArchCSpacePre_AI.thy | 2 +- .../RISCV64/ArchCSpace_AI.thy | 2 +- .../RISCV64/ArchDetSchedAux_AI.thy | 2 +- .../RISCV64/ArchDetSchedDomainTime_AI.thy | 2 +- .../RISCV64/ArchDetSchedSchedule_AI.thy | 2 +- .../RISCV64/ArchDeterministic_AI.thy | 2 +- .../RISCV64/ArchDetype_AI.thy | 2 +- .../RISCV64/ArchEmptyFail_AI.thy | 2 +- .../RISCV64/ArchFinalise_AI.thy | 2 +- .../RISCV64/ArchInterruptAcc_AI.thy | 2 +- .../RISCV64/ArchInterrupt_AI.thy | 2 +- .../RISCV64/ArchInvariants_AI.thy | 2 +- .../RISCV64/ArchIpcCancel_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchIpc_AI.thy | 2 +- .../RISCV64/ArchKHeap_AI.thy | 2 +- .../RISCV64/ArchKernelInit_AI.thy | 6 +++--- .../RISCV64/ArchRetype_AI.thy | 2 +- .../RISCV64/ArchSchedule_AI.thy | 2 +- .../RISCV64/ArchSyscall_AI.thy | 2 +- .../RISCV64/ArchTcbAcc_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchTcb_AI.thy | 2 +- .../RISCV64/ArchUntyped_AI.thy | 2 +- .../RISCV64/ArchVSpaceEntries_AI.thy | 2 +- .../RISCV64/ArchVSpace_AI.thy | 2 +- .../invariant-abstract/RISCV64/Machine_AI.thy | 2 +- proof/invariant-abstract/Syscall_AI.thy | 8 ++++---- proof/invariant-abstract/TcbAcc_AI.thy | 2 +- proof/invariant-abstract/Tcb_AI.thy | 2 +- proof/invariant-abstract/Untyped_AI.thy | 3 ++- proof/invariant-abstract/VSpaceEntries_AI.thy | 2 +- proof/invariant-abstract/VSpacePre_AI.thy | 2 +- proof/invariant-abstract/VSpace_AI.thy | 2 +- proof/invariant-abstract/X64/ArchADT_AI.thy | 2 +- proof/invariant-abstract/X64/ArchAInvsPre.thy | 2 +- proof/invariant-abstract/X64/ArchAcc_AI.thy | 3 ++- proof/invariant-abstract/X64/ArchArch_AI.thy | 2 +- .../invariant-abstract/X64/ArchBCorres2_AI.thy | 2 +- .../invariant-abstract/X64/ArchBCorres_AI.thy | 2 +- proof/invariant-abstract/X64/ArchBits_AI.thy | 2 +- .../invariant-abstract/X64/ArchCNodeInv_AI.thy | 2 +- .../X64/ArchCSpaceInvPre_AI.thy | 2 +- .../X64/ArchCSpaceInv_AI.thy | 2 +- .../X64/ArchCSpacePre_AI.thy | 2 +- proof/invariant-abstract/X64/ArchCSpace_AI.thy | 2 +- .../X64/ArchDetSchedAux_AI.thy | 2 +- .../X64/ArchDetSchedDomainTime_AI.thy | 2 +- .../X64/ArchDetSchedSchedule_AI.thy | 2 +- .../X64/ArchDeterministic_AI.thy | 2 +- proof/invariant-abstract/X64/ArchDetype_AI.thy | 2 +- .../X64/ArchEmptyFail_AI.thy | 2 +- .../invariant-abstract/X64/ArchFinalise_AI.thy | 2 +- .../X64/ArchInterruptAcc_AI.thy | 2 +- .../X64/ArchInterrupt_AI.thy | 2 +- .../X64/ArchInvariants_AI.thy | 2 +- .../X64/ArchIpcCancel_AI.thy | 2 +- proof/invariant-abstract/X64/ArchIpc_AI.thy | 2 +- proof/invariant-abstract/X64/ArchKHeap_AI.thy | 2 +- .../X64/ArchKernelInit_AI.thy | 6 +++--- proof/invariant-abstract/X64/ArchRetype_AI.thy | 2 +- .../invariant-abstract/X64/ArchSchedule_AI.thy | 2 +- .../invariant-abstract/X64/ArchSyscall_AI.thy | 2 +- proof/invariant-abstract/X64/ArchTcbAcc_AI.thy | 2 +- proof/invariant-abstract/X64/ArchTcb_AI.thy | 2 +- .../invariant-abstract/X64/ArchUntyped_AI.thy | 2 +- .../X64/ArchVSpaceEntries_AI.thy | 2 +- .../X64/ArchVSpaceLookup_AI.thy | 5 +++-- proof/invariant-abstract/X64/ArchVSpace_AI.thy | 2 +- proof/invariant-abstract/X64/Machine_AI.thy | 2 +- proof/refine/ARM/ArchMove_R.thy | 3 +-- proof/refine/ARM_HYP/ArchMove_R.thy | 3 +-- proof/refine/RISCV64/ArchMove_R.thy | 3 +-- proof/refine/X64/ArchMove_R.thy | 3 +-- spec/abstract/ARM/ArchDecode_A.thy | 4 ++-- spec/abstract/ARM/ArchFault_A.thy | 2 +- spec/abstract/ARM/ArchInterrupt_A.thy | 2 +- spec/abstract/ARM/ArchInvocation_A.thy | 2 +- spec/abstract/ARM/ArchIpcCancel_A.thy | 3 +-- spec/abstract/ARM/ArchTcb_A.thy | 2 +- spec/abstract/ARM/ArchVSpaceAcc_A.thy | 2 +- spec/abstract/ARM/ArchVSpace_A.thy | 2 +- spec/abstract/ARM/Arch_A.thy | 2 +- spec/abstract/ARM/Arch_Structs_A.thy | 4 ++-- spec/abstract/ARM/Hypervisor_A.thy | 2 +- spec/abstract/ARM/Init_A.thy | 2 +- spec/abstract/ARM_HYP/ArchDecode_A.thy | 2 +- spec/abstract/ARM_HYP/ArchFault_A.thy | 2 +- spec/abstract/ARM_HYP/ArchInterrupt_A.thy | 2 +- spec/abstract/ARM_HYP/ArchInvocation_A.thy | 2 +- spec/abstract/ARM_HYP/ArchIpcCancel_A.thy | 3 +-- spec/abstract/ARM_HYP/ArchTcb_A.thy | 2 +- spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy | 2 +- spec/abstract/ARM_HYP/ArchVSpace_A.thy | 4 ++-- spec/abstract/ARM_HYP/Arch_A.thy | 3 +-- spec/abstract/ARM_HYP/Arch_Structs_A.thy | 4 ++-- spec/abstract/ARM_HYP/Hypervisor_A.thy | 2 +- spec/abstract/ARM_HYP/Init_A.thy | 2 +- spec/abstract/ARM_HYP/VCPU_A.thy | 6 +++--- spec/abstract/CSpace_A.thy | 4 ++-- spec/abstract/Decode_A.thy | 2 +- spec/abstract/Interrupt_A.thy | 2 +- spec/abstract/Invocations_A.thy | 2 +- spec/abstract/IpcCancel_A.thy | 3 +-- spec/abstract/Ipc_A.thy | 2 +- spec/abstract/KernelInit_A.thy | 2 +- spec/abstract/MiscMachine_A.thy | 2 +- spec/abstract/RISCV64/ArchDecode_A.thy | 4 ++-- spec/abstract/RISCV64/ArchFault_A.thy | 2 +- spec/abstract/RISCV64/ArchInterrupt_A.thy | 2 +- spec/abstract/RISCV64/ArchInvocation_A.thy | 2 +- spec/abstract/RISCV64/ArchIpcCancel_A.thy | 2 +- spec/abstract/RISCV64/ArchTcb_A.thy | 2 +- spec/abstract/RISCV64/ArchVSpaceAcc_A.thy | 2 +- spec/abstract/RISCV64/ArchVSpace_A.thy | 2 +- spec/abstract/RISCV64/Arch_A.thy | 2 +- spec/abstract/RISCV64/Arch_Structs_A.thy | 4 ++-- spec/abstract/RISCV64/Hypervisor_A.thy | 2 +- spec/abstract/RISCV64/Init_A.thy | 5 +++-- spec/abstract/Retype_A.thy | 4 ++-- spec/abstract/Schedule_A.thy | 2 +- spec/abstract/Structures_A.thy | 3 +-- spec/abstract/Syscall_A.thy | 4 ++-- spec/abstract/Tcb_A.thy | 2 +- spec/abstract/X64/ArchDecode_A.thy | 4 ++-- spec/abstract/X64/ArchFault_A.thy | 2 +- spec/abstract/X64/ArchInterrupt_A.thy | 2 +- spec/abstract/X64/ArchInvocation_A.thy | 2 +- spec/abstract/X64/ArchIpcCancel_A.thy | 3 +-- spec/abstract/X64/ArchTcb_A.thy | 2 +- spec/abstract/X64/ArchVSpaceAcc_A.thy | 2 +- spec/abstract/X64/ArchVSpace_A.thy | 2 +- spec/abstract/X64/Arch_A.thy | 2 +- spec/abstract/X64/Arch_Structs_A.thy | 4 ++-- spec/abstract/X64/Hypervisor_A.thy | 2 +- spec/abstract/X64/Init_A.thy | 2 +- spec/cspec/KernelInc_C.thy | 8 ++++---- spec/design/m-skel/ARM/MachineTypes.thy | 2 +- spec/design/m-skel/ARM_HYP/MachineTypes.thy | 2 +- spec/design/skel/ARM/ArchFaultHandler_H.thy | 2 +- spec/design/skel/ARM/ArchFault_H.thy | 2 +- spec/design/skel/ARM/ArchHypervisor_H.thy | 6 +++--- spec/design/skel/ARM/ArchIntermediate_H.thy | 2 +- spec/design/skel/ARM/ArchInterruptDecls_H.thy | 2 +- spec/design/skel/ARM/ArchInterrupt_H.thy | 6 +++--- .../design/skel/ARM/ArchInvocationLabels_H.thy | 2 +- spec/design/skel/ARM/ArchLabelFuns_H.thy | 2 +- spec/design/skel/ARM/ArchObjInsts_H.thy | 4 ++-- spec/design/skel/ARM/ArchRetypeDecls_H.thy | 8 ++++---- spec/design/skel/ARM/ArchRetype_H.thy | 2 +- spec/design/skel/ARM/ArchStructures_H.thy | 2 +- spec/design/skel/ARM/ArchTCB_H.thy | 2 +- spec/design/skel/ARM/ArchThreadDecls_H.thy | 6 +++--- spec/design/skel/ARM/ArchThread_H.thy | 2 +- spec/design/skel/ARM/ArchVSpaceDecls_H.thy | 2 +- spec/design/skel/ARM/ArchVSpace_H.thy | 6 +++--- spec/design/skel/ARM/Arch_Structs_B.thy | 2 +- spec/design/skel/ARM/Hardware_H.thy | 2 +- spec/design/skel/ARM/RegisterSet_H.thy | 2 +- spec/design/skel/ARM/State_H.thy | 2 +- .../design/skel/ARM_HYP/ArchFaultHandler_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchFault_H.thy | 4 +--- spec/design/skel/ARM_HYP/ArchHypervisor_H.thy | 6 +++--- .../design/skel/ARM_HYP/ArchIntermediate_H.thy | 2 +- .../skel/ARM_HYP/ArchInterruptDecls_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchInterrupt_H.thy | 6 +++--- .../skel/ARM_HYP/ArchInvocationLabels_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchLabelFuns_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchObjInsts_H.thy | 4 ++-- spec/design/skel/ARM_HYP/ArchRetypeDecls_H.thy | 8 ++++---- spec/design/skel/ARM_HYP/ArchRetype_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchStructures_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchTCB_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchThreadDecls_H.thy | 6 +++--- spec/design/skel/ARM_HYP/ArchThread_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchVSpaceDecls_H.thy | 2 +- spec/design/skel/ARM_HYP/ArchVSpace_H.thy | 4 ++-- spec/design/skel/ARM_HYP/Arch_Structs_B.thy | 2 +- spec/design/skel/ARM_HYP/Hardware_H.thy | 2 +- spec/design/skel/ARM_HYP/RegisterSet_H.thy | 2 +- spec/design/skel/ARM_HYP/State_H.thy | 2 +- spec/design/skel/ARM_HYP/VCPU_H.thy | 8 +++++--- spec/design/skel/Event_H.thy | 2 +- spec/design/skel/FaultHandler_H.thy | 6 ++++-- spec/design/skel/Fault_H.thy | 2 +- spec/design/skel/Hypervisor_H.thy | 2 +- spec/design/skel/Interrupt_H.thy | 2 +- spec/design/skel/InvocationLabels_H.thy | 2 +- spec/design/skel/Invocations_H.thy | 4 ++-- spec/design/skel/KernelInit_H.thy | 2 +- spec/design/skel/KernelStateData_H.thy | 4 ++-- spec/design/skel/ObjectInstances_H.thy | 2 +- .../design/skel/RISCV64/ArchFaultHandler_H.thy | 2 +- spec/design/skel/RISCV64/ArchFault_H.thy | 2 +- spec/design/skel/RISCV64/ArchHypervisor_H.thy | 6 +++--- .../design/skel/RISCV64/ArchIntermediate_H.thy | 2 +- .../skel/RISCV64/ArchInterruptDecls_H.thy | 2 +- spec/design/skel/RISCV64/ArchInterrupt_H.thy | 6 +++--- .../skel/RISCV64/ArchInvocationLabels_H.thy | 2 +- spec/design/skel/RISCV64/ArchLabelFuns_H.thy | 2 +- spec/design/skel/RISCV64/ArchObjInsts_H.thy | 4 ++-- spec/design/skel/RISCV64/ArchRetypeDecls_H.thy | 8 ++++---- spec/design/skel/RISCV64/ArchRetype_H.thy | 2 +- spec/design/skel/RISCV64/ArchStructures_H.thy | 2 +- spec/design/skel/RISCV64/ArchTCB_H.thy | 2 +- spec/design/skel/RISCV64/ArchThreadDecls_H.thy | 6 +++--- spec/design/skel/RISCV64/ArchThread_H.thy | 3 +-- spec/design/skel/RISCV64/ArchVSpaceDecls_H.thy | 2 +- spec/design/skel/RISCV64/ArchVSpace_H.thy | 6 +++--- spec/design/skel/RISCV64/Arch_Structs_B.thy | 2 +- spec/design/skel/RISCV64/Hardware_H.thy | 2 +- spec/design/skel/RISCV64/RegisterSet_H.thy | 2 +- spec/design/skel/RetypeDecls_H.thy | 2 +- spec/design/skel/Structures_H.thy | 4 ++-- spec/design/skel/TCB_H.thy | 2 +- spec/design/skel/ThreadDecls_H.thy | 2 +- spec/design/skel/Thread_H.thy | 2 +- spec/design/skel/Types_H.thy | 4 ++-- spec/design/skel/Untyped_H.thy | 2 +- spec/design/skel/VSpace_H.thy | 2 +- spec/design/skel/X64/ArchFaultHandler_H.thy | 2 +- spec/design/skel/X64/ArchFault_H.thy | 2 +- spec/design/skel/X64/ArchHook_H.thy | 2 +- spec/design/skel/X64/ArchHypervisor_H.thy | 8 ++++---- spec/design/skel/X64/ArchIntermediate_H.thy | 2 +- spec/design/skel/X64/ArchInterruptDecls_H.thy | 2 +- spec/design/skel/X64/ArchInterrupt_H.thy | 6 +++--- .../design/skel/X64/ArchInvocationLabels_H.thy | 2 +- spec/design/skel/X64/ArchLabelFuns_H.thy | 2 +- spec/design/skel/X64/ArchObjInsts_H.thy | 4 ++-- spec/design/skel/X64/ArchRetypeDecls_H.thy | 8 ++++---- spec/design/skel/X64/ArchRetype_H.thy | 2 +- spec/design/skel/X64/ArchStructures_H.thy | 2 +- spec/design/skel/X64/ArchTCB_H.thy | 2 +- spec/design/skel/X64/ArchThreadDecls_H.thy | 6 +++--- spec/design/skel/X64/ArchThread_H.thy | 2 +- spec/design/skel/X64/ArchVSpaceDecls_H.thy | 2 +- spec/design/skel/X64/ArchVSpace_H.thy | 6 +++--- spec/design/skel/X64/Arch_Structs_B.thy | 2 +- spec/design/skel/X64/Hardware_H.thy | 2 +- spec/design/skel/X64/RegisterSet_H.thy | 2 +- spec/machine/ARM/MachineOps.thy | 2 +- spec/machine/ARM/Platform.thy | 2 +- spec/machine/ARM_HYP/MachineOps.thy | 2 +- spec/machine/ARM_HYP/Platform.thy | 2 +- spec/machine/MachineExports.thy | 2 +- spec/machine/MachineMonad.thy | 2 +- spec/machine/RISCV64/MachineOps.thy | 2 +- spec/machine/RISCV64/Platform.thy | 2 +- spec/machine/X64/MachineOps.thy | 2 +- spec/machine/X64/Platform.thy | 2 +- tools/asmrefine/CommonOps.thy | 8 ++++---- tools/c-parser/CProof.thy | 6 +++--- tools/c-parser/Simpl/Simpl.thy | 18 +++++++++--------- tools/c-parser/Simpl/ex/Closure.thy | 2 +- tools/c-parser/Simpl/ex/ClosureEx.thy | 2 +- tools/c-parser/Simpl/ex/Compose.thy | 2 +- tools/c-parser/Simpl/ex/ComposeEx.thy | 2 +- tools/c-parser/Simpl/ex/ProcParEx.thy | 2 +- tools/c-parser/Simpl/ex/ProcParExSP.thy | 2 +- tools/c-parser/Simpl/ex/Quicksort.thy | 2 +- tools/c-parser/Simpl/ex/VcgEx.thy | 2 +- tools/c-parser/Simpl/ex/VcgExSP.thy | 2 +- tools/c-parser/Simpl/ex/VcgExTotal.thy | 2 +- tools/c-parser/Simpl/ex/XVcgEx.thy | 2 +- tools/c-parser/testfiles/factorial.thy | 2 +- tools/c-parser/testfiles/kmalloc.thy | 2 +- tools/c-parser/testfiles/list_reverse.thy | 2 +- tools/c-parser/testfiles/list_reverse_norm.thy | 2 +- .../umm_heap/ARM/ArchArraysMemInstance.thy | 2 +- .../umm_heap/ARM/Word_Mem_Encoding.thy | 2 +- .../umm_heap/ARM_HYP/ArchArraysMemInstance.thy | 2 +- .../umm_heap/ARM_HYP/Word_Mem_Encoding.thy | 2 +- tools/c-parser/umm_heap/ArrayAssertion.thy | 2 +- tools/c-parser/umm_heap/CTypesBase.thy | 2 +- .../umm_heap/RISCV64/ArchArraysMemInstance.thy | 2 +- .../umm_heap/RISCV64/Word_Mem_Encoding.thy | 2 +- tools/c-parser/umm_heap/TypHeap.thy | 2 +- tools/c-parser/umm_heap/Vanilla32.thy | 2 +- .../umm_heap/X64/ArchArraysMemInstance.thy | 2 +- .../umm_heap/X64/Word_Mem_Encoding.thy | 2 +- 453 files changed, 596 insertions(+), 598 deletions(-) diff --git a/camkes/glue-spec/example-dataport/GenDataportBase.thy b/camkes/glue-spec/example-dataport/GenDataportBase.thy index 40a0832de..17a14577f 100644 --- a/camkes/glue-spec/example-dataport/GenDataportBase.thy +++ b/camkes/glue-spec/example-dataport/GenDataportBase.thy @@ -7,7 +7,7 @@ chapter \\label{h:dataportbase}Example -- Dataports\ (*<*) (* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *) theory GenDataportBase -imports "../Types" "../Abbreviations" "../Connector" +imports "Types" "Abbreviations" "Connector" begin (*>*) diff --git a/camkes/glue-spec/example-dataport/UserDataport.thy b/camkes/glue-spec/example-dataport/UserDataport.thy index 41c22d434..7f3be370c 100644 --- a/camkes/glue-spec/example-dataport/UserDataport.thy +++ b/camkes/glue-spec/example-dataport/UserDataport.thy @@ -5,7 +5,7 @@ *) (*<*) theory UserDataport -imports "../UserStubs" GenDataportBase +imports "UserStubs" GenDataportBase begin (* Stub to expose existing static UserStubs.thy. This is to avoid having to diff --git a/camkes/glue-spec/example-event/GenEventBase.thy b/camkes/glue-spec/example-event/GenEventBase.thy index 36475eb17..161978237 100644 --- a/camkes/glue-spec/example-event/GenEventBase.thy +++ b/camkes/glue-spec/example-event/GenEventBase.thy @@ -7,7 +7,7 @@ chapter \\label{s:eventbase}Example -- Events\ (*<*) (* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *) theory GenEventBase -imports "../Types" "../Abbreviations" "../Connector" +imports "Types" "Abbreviations" "Connector" begin (*>*) diff --git a/camkes/glue-spec/example-event/UserEvent.thy b/camkes/glue-spec/example-event/UserEvent.thy index 3cac1d061..ada1c81d5 100644 --- a/camkes/glue-spec/example-event/UserEvent.thy +++ b/camkes/glue-spec/example-event/UserEvent.thy @@ -5,7 +5,7 @@ *) (*<*) theory UserEvent -imports "../UserStubs" GenEventBase +imports "UserStubs" GenEventBase begin (* Stub to expose existing static UserStubs.thy. This is to avoid having to diff --git a/camkes/glue-spec/example-procedure/GenSimpleBase.thy b/camkes/glue-spec/example-procedure/GenSimpleBase.thy index a225a4055..f1dd50e3f 100644 --- a/camkes/glue-spec/example-procedure/GenSimpleBase.thy +++ b/camkes/glue-spec/example-procedure/GenSimpleBase.thy @@ -7,7 +7,7 @@ chapter \\label{h:procbase}Example -- Procedures\ (*<*) (* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *) theory GenSimpleBase -imports "../Types" "../Abbreviations" "../Connector" +imports "Types" "Abbreviations" "Connector" begin (*>*) diff --git a/camkes/glue-spec/example-procedure/UserSimple.thy b/camkes/glue-spec/example-procedure/UserSimple.thy index 999cf27a0..c81d2a6b0 100644 --- a/camkes/glue-spec/example-procedure/UserSimple.thy +++ b/camkes/glue-spec/example-procedure/UserSimple.thy @@ -5,7 +5,7 @@ *) (*<*) theory UserSimple -imports "../UserStubs" GenSimpleBase +imports "UserStubs" GenSimpleBase begin (* Stub to expose existing static UserStubs.thy. This is to avoid having to diff --git a/camkes/glue-spec/example-trusted/GenFilter2Base.thy b/camkes/glue-spec/example-trusted/GenFilter2Base.thy index c6f9d697d..b338e0f84 100644 --- a/camkes/glue-spec/example-trusted/GenFilter2Base.thy +++ b/camkes/glue-spec/example-trusted/GenFilter2Base.thy @@ -6,7 +6,7 @@ (*<*) (* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *) theory GenFilter2Base -imports "../Types" "../Abbreviations" "../Connector" +imports "Types" "Abbreviations" "Connector" begin (* Connections *) diff --git a/camkes/glue-spec/example-trusted/UserFilter2.thy b/camkes/glue-spec/example-trusted/UserFilter2.thy index 2a1c1b428..af272e7fd 100644 --- a/camkes/glue-spec/example-trusted/UserFilter2.thy +++ b/camkes/glue-spec/example-trusted/UserFilter2.thy @@ -5,7 +5,7 @@ *) (*<*) theory UserFilter2 -imports GenFilter2Base "../UserStubs" +imports GenFilter2Base "UserStubs" begin (*>*) diff --git a/camkes/glue-spec/example-untrusted/GenFilterBase.thy b/camkes/glue-spec/example-untrusted/GenFilterBase.thy index 8a6d41c09..3b9202c34 100644 --- a/camkes/glue-spec/example-untrusted/GenFilterBase.thy +++ b/camkes/glue-spec/example-untrusted/GenFilterBase.thy @@ -8,7 +8,7 @@ chapter \\label{h:filter}Example -- System Level Reasoning\ (*<*) (* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *) theory GenFilterBase -imports "../Types" "../Abbreviations" "../Connector" +imports "Types" "Abbreviations" "Connector" begin (*>*) diff --git a/camkes/glue-spec/example-untrusted/UserFilter.thy b/camkes/glue-spec/example-untrusted/UserFilter.thy index 999d99540..61af033b5 100644 --- a/camkes/glue-spec/example-untrusted/UserFilter.thy +++ b/camkes/glue-spec/example-untrusted/UserFilter.thy @@ -5,7 +5,7 @@ *) (*<*) theory UserFilter -imports "../UserStubs" GenFilterBase +imports "UserStubs" GenFilterBase begin (* Stub to expose existing static UserStubs.thy. This is to avoid having to diff --git a/lib/Apply_Trace.thy b/lib/Apply_Trace.thy index a4b0d5ac0..35eb5a579 100644 --- a/lib/Apply_Trace.thy +++ b/lib/Apply_Trace.thy @@ -9,7 +9,7 @@ theory Apply_Trace imports Main - "ml-helpers/MLUtils" + "MLUtils" begin diff --git a/lib/AutoLevity.thy b/lib/AutoLevity.thy index aac06bccc..8fea98eae 100644 --- a/lib/AutoLevity.thy +++ b/lib/AutoLevity.thy @@ -5,7 +5,7 @@ *) theory AutoLevity (* FIXME: broken *) -imports "../tools/proofcount/ProofGraph" +imports "ProofGraph" begin ML \val infoflow_file = "~~/../lib/proof_counting/Noninterference_Refinement_graphs.xml"\ ML \val (full_spec,proof_spec_raw,thy_deps) = Proof_Graph.read_graph_spec_from infoflow_file\ diff --git a/lib/BCorres_UL.thy b/lib/BCorres_UL.thy index 138675aac..c231e7226 100644 --- a/lib/BCorres_UL.thy +++ b/lib/BCorres_UL.thy @@ -6,7 +6,7 @@ theory BCorres_UL imports - "Monad_WP/NonDetMonadVCG" + NonDetMonadVCG Crunch_Instances_NonDet begin diff --git a/lib/Bisim_UL.thy b/lib/Bisim_UL.thy index af3292628..369e22119 100644 --- a/lib/Bisim_UL.thy +++ b/lib/Bisim_UL.thy @@ -8,7 +8,7 @@ theory Bisim_UL imports - "Monad_WP/NonDetMonadVCG" + NonDetMonadVCG Corres_UL EmptyFailLib begin diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index 74a929b0a..71ec656a6 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -7,8 +7,8 @@ theory Corres_UL imports Crunch_Instances_NonDet - "Monad_WP/wp/WPEx" - "Monad_WP/wp/WPFix" + WPEx + WPFix HaskellLemmaBucket begin diff --git a/lib/Crunch.thy b/lib/Crunch.thy index d98d780bb..f96ca836e 100644 --- a/lib/Crunch.thy +++ b/lib/Crunch.thy @@ -6,9 +6,9 @@ theory Crunch imports - "Monad_WP/wp/WPSimp" + WPSimp Lib - "ml-helpers/MLUtils" + MLUtils keywords "crunch" "crunch_ignore" "crunches" :: thy_decl begin diff --git a/lib/Crunch_Instances_NonDet.thy b/lib/Crunch_Instances_NonDet.thy index abaf5a682..a2b441173 100644 --- a/lib/Crunch_Instances_NonDet.thy +++ b/lib/Crunch_Instances_NonDet.thy @@ -7,8 +7,8 @@ theory Crunch_Instances_NonDet imports Crunch - "Monad_WP/wp/WPEx" - "Monad_WP/NonDetMonadVCG" + WPEx + NonDetMonadVCG begin lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy index 87a9822db..458d26dfc 100644 --- a/lib/Crunch_Instances_Trace.thy +++ b/lib/Crunch_Instances_Trace.thy @@ -7,7 +7,7 @@ theory Crunch_Instances_Trace imports Crunch - "Monad_WP/TraceMonadVCG" + TraceMonadVCG begin lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE diff --git a/lib/Eisbach_Methods.thy b/lib/Eisbach_Methods.thy index 2e83158aa..cbc573226 100644 --- a/lib/Eisbach_Methods.thy +++ b/lib/Eisbach_Methods.thy @@ -10,7 +10,7 @@ theory Eisbach_Methods imports - "subgoal_focus/Subgoal_Methods" + Subgoal_Methods "HOL-Eisbach.Eisbach_Tools" Rule_By_Method Local_Method diff --git a/lib/EmptyFailLib.thy b/lib/EmptyFailLib.thy index 48c1ffa21..b8b93f7e5 100644 --- a/lib/EmptyFailLib.thy +++ b/lib/EmptyFailLib.thy @@ -6,7 +6,7 @@ theory EmptyFailLib imports - "Monad_WP/NonDetMonad" + NonDetMonad HaskellLib_H begin diff --git a/lib/FP_Eval.thy b/lib/FP_Eval.thy index b5eed2082..a98409483 100644 --- a/lib/FP_Eval.thy +++ b/lib/FP_Eval.thy @@ -7,7 +7,7 @@ theory FP_Eval imports HOL.HOL - "ml-helpers/TermPatternAntiquote" + TermPatternAntiquote begin text \ diff --git a/lib/GenericLib.thy b/lib/GenericLib.thy index 80c3c1767..18eb72ba1 100644 --- a/lib/GenericLib.thy +++ b/lib/GenericLib.thy @@ -7,7 +7,7 @@ theory GenericLib imports Crunch_Instances_NonDet - "Monad_WP/wp/WPEx" + WPEx HaskellLemmaBucket begin diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy index a22f8c451..8290cfc12 100644 --- a/lib/HaskellLib_H.thy +++ b/lib/HaskellLib_H.thy @@ -13,8 +13,8 @@ theory HaskellLib_H imports Lib NatBitwise - "More_Numeral_Type" - "Monad_WP/NonDetMonadVCG" + More_Numeral_Type + NonDetMonadVCG begin abbreviation (input) "flip \ swp" diff --git a/lib/ML_Goal_Test.thy b/lib/ML_Goal_Test.thy index 2b98fc4b5..989ff7f68 100644 --- a/lib/ML_Goal_Test.thy +++ b/lib/ML_Goal_Test.thy @@ -7,7 +7,7 @@ theory ML_Goal_Test imports ML_Goal - "ml-helpers/MLUtils" + MLUtils begin experiment begin diff --git a/lib/MonadEq.thy b/lib/MonadEq.thy index a874d8816..fff338c73 100644 --- a/lib/MonadEq.thy +++ b/lib/MonadEq.thy @@ -20,7 +20,7 @@ * are added to the "monad_eq" set. *) theory MonadEq -imports "Monad_WP/NonDetMonadVCG" +imports NonDetMonadVCG begin (* Setup "monad_eq" attributes. *) diff --git a/lib/Monad_WP/Datatype_Schematic.thy b/lib/Monad_WP/Datatype_Schematic.thy index 46cd3e1eb..89da8810f 100644 --- a/lib/Monad_WP/Datatype_Schematic.thy +++ b/lib/Monad_WP/Datatype_Schematic.thy @@ -6,8 +6,8 @@ theory Datatype_Schematic imports - "../ml-helpers/MLUtils" - "../ml-helpers/TermPatternAntiquote" + MLUtils + TermPatternAntiquote begin text \ diff --git a/lib/Monad_WP/NonDetMonad.thy b/lib/Monad_WP/NonDetMonad.thy index 85fe8cdd4..9ee95bba4 100644 --- a/lib/Monad_WP/NonDetMonad.thy +++ b/lib/Monad_WP/NonDetMonad.thy @@ -11,7 +11,7 @@ chapter "Nondeterministic State Monad with Failure" theory NonDetMonad -imports "../Lib" +imports Lib begin text \ diff --git a/lib/Monad_WP/NonDetMonadVCG.thy b/lib/Monad_WP/NonDetMonadVCG.thy index 0e707f7d4..cbaf8a66b 100644 --- a/lib/Monad_WP/NonDetMonadVCG.thy +++ b/lib/Monad_WP/NonDetMonadVCG.thy @@ -7,8 +7,8 @@ theory NonDetMonadVCG imports NonDetMonadLemmas - "wp/WPSimp" - "Strengthen" + WPSimp + Strengthen begin declare K_def [simp] diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy index e52712f86..9be83738a 100644 --- a/lib/Monad_WP/OptionMonad.thy +++ b/lib/Monad_WP/OptionMonad.thy @@ -12,8 +12,8 @@ theory OptionMonad (* FIXME: this is really a Reader_Option_Monad *) imports - "../Lib" (* FIXME: reduce dependencies *) - "Less_Monad_Syntax" + Lib (* FIXME: reduce dependencies *) + Less_Monad_Syntax begin type_synonym ('s,'a) lookup = "'s \ 'a option" diff --git a/lib/Monad_WP/OptionMonadWP.thy b/lib/Monad_WP/OptionMonadWP.thy index 0a0e8be13..d84d20a3e 100644 --- a/lib/Monad_WP/OptionMonadWP.thy +++ b/lib/Monad_WP/OptionMonadWP.thy @@ -13,7 +13,7 @@ This list is almost certainly incomplete; add rules here as they are needed. theory OptionMonadWP imports OptionMonadND - "wp/WP" + WP begin declare K_def [simp] diff --git a/lib/Monad_WP/TraceMonad.thy b/lib/Monad_WP/TraceMonad.thy index c61aa2442..3e2d53de1 100644 --- a/lib/Monad_WP/TraceMonad.thy +++ b/lib/Monad_WP/TraceMonad.thy @@ -5,8 +5,8 @@ *) theory TraceMonad imports - "../Lib" - "Strengthen" + Lib + Strengthen begin text \ diff --git a/lib/Monad_WP/TraceMonadVCG.thy b/lib/Monad_WP/TraceMonadVCG.thy index 9ef1dcb0f..ffb39a307 100644 --- a/lib/Monad_WP/TraceMonadVCG.thy +++ b/lib/Monad_WP/TraceMonadVCG.thy @@ -6,8 +6,8 @@ theory TraceMonadVCG imports TraceMonad - "wp/WPSimp" - "Strengthen" + WPSimp + Strengthen begin lemma trace_steps_append: diff --git a/lib/Monad_WP/wp/Eisbach_WP.thy b/lib/Monad_WP/wp/Eisbach_WP.thy index 9578f8236..a4c7483b0 100644 --- a/lib/Monad_WP/wp/Eisbach_WP.thy +++ b/lib/Monad_WP/wp/Eisbach_WP.thy @@ -8,11 +8,11 @@ theory Eisbach_WP imports - "../../Eisbach_Methods" - "../NonDetMonadVCG" - "../../Conjuncts" - "../../Rule_By_Method" - "WPI" + Eisbach_Methods + NonDetMonadVCG + Conjuncts + Rule_By_Method + WPI begin diff --git a/lib/Monad_WP/wp/WP.thy b/lib/Monad_WP/wp/WP.thy index d163a3d3e..66ef60f11 100644 --- a/lib/Monad_WP/wp/WP.thy +++ b/lib/Monad_WP/wp/WP.thy @@ -6,10 +6,10 @@ theory WP imports - "WP_Pre" - "WPFix" - "../../Apply_Debug" - "../../ml-helpers/MLUtils" + WP_Pre + WPFix + Apply_Debug + MLUtils begin definition diff --git a/lib/Monad_WP/wp/WPBang.thy b/lib/Monad_WP/wp/WPBang.thy index c64f98593..0c739478a 100644 --- a/lib/Monad_WP/wp/WPBang.thy +++ b/lib/Monad_WP/wp/WPBang.thy @@ -7,8 +7,8 @@ theory WPBang imports WP - "../../ProvePart" - "../NonDetMonadVCG" + ProvePart + NonDetMonadVCG begin lemma conj_meta_forward: diff --git a/lib/Monad_WP/wp/WPEx.thy b/lib/Monad_WP/wp/WPEx.thy index b6e545e70..2760e2552 100644 --- a/lib/Monad_WP/wp/WPEx.thy +++ b/lib/Monad_WP/wp/WPEx.thy @@ -6,8 +6,8 @@ theory WPEx imports - "../NonDetMonadVCG" - "../Strengthen" + NonDetMonadVCG + Strengthen begin text \WPEx - the WP Extension Experiment\ diff --git a/lib/Monad_WP/wp/WPFix.thy b/lib/Monad_WP/wp/WPFix.thy index 7012e60c1..00d0042b0 100644 --- a/lib/Monad_WP/wp/WPFix.thy +++ b/lib/Monad_WP/wp/WPFix.thy @@ -6,8 +6,8 @@ theory WPFix imports - "../Datatype_Schematic" - "../Strengthen" + Datatype_Schematic + Strengthen begin diff --git a/lib/Monad_WP/wp/WPI.thy b/lib/Monad_WP/wp/WPI.thy index e5eb4a828..748701136 100644 --- a/lib/Monad_WP/wp/WPI.thy +++ b/lib/Monad_WP/wp/WPI.thy @@ -32,9 +32,9 @@ theory WPI imports - "../../Eisbach_Methods" - "../NonDetMonadLemmas" - "WPEx" + Eisbach_Methods + NonDetMonadLemmas + WPEx begin text \The ML version of repeat_new is slightly faster than the Eisbach one.\ diff --git a/lib/Monad_WP/wp/WPSimp.thy b/lib/Monad_WP/wp/WPSimp.thy index 2790e14b9..d18b905e3 100644 --- a/lib/Monad_WP/wp/WPSimp.thy +++ b/lib/Monad_WP/wp/WPSimp.thy @@ -9,7 +9,7 @@ imports "WP" "WPC" "WPFix" - "../../Simp_No_Conditional" + Simp_No_Conditional begin (* Wrap up the standard usage pattern of wp/wpc/simp into its own command: *) diff --git a/lib/Monad_WP/wp/WP_Pre.thy b/lib/Monad_WP/wp/WP_Pre.thy index b1927dcd0..87f5311bc 100644 --- a/lib/Monad_WP/wp/WP_Pre.thy +++ b/lib/Monad_WP/wp/WP_Pre.thy @@ -7,7 +7,7 @@ theory WP_Pre imports Main - "../../Trace_Schematic_Insts" + Trace_Schematic_Insts "HOL-Eisbach.Eisbach_Tools" begin diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy index 07ed04495..0733978ac 100644 --- a/lib/MonadicRewrite.thy +++ b/lib/MonadicRewrite.thy @@ -8,7 +8,7 @@ theory MonadicRewrite imports - "Monad_WP/NonDetMonadVCG" + NonDetMonadVCG Corres_UL EmptyFailLib LemmaBucket diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index b148c9f6a..897394cdf 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -6,9 +6,9 @@ theory NonDetMonadLemmaBucket imports - "Monad_WP/NonDetMonadVCG" - "MonadEq" - "Monad_WP/WhileLoopRulesCompleteness" + NonDetMonadVCG + MonadEq + WhileLoopRulesCompleteness "Word_Lib.Distinct_Prop" begin setup \AutoLevity_Base.add_attribute_test "wp" WeakestPre.is_wp_rule\ diff --git a/lib/RangeMap.thy b/lib/RangeMap.thy index 95cdb2a7f..29b92dfd3 100644 --- a/lib/RangeMap.thy +++ b/lib/RangeMap.thy @@ -8,7 +8,7 @@ theory RangeMap imports FastMap FP_Eval - "ml-helpers/MkTermAntiquote" + MkTermAntiquote begin text \ diff --git a/lib/Trace_Schematic_Insts.thy b/lib/Trace_Schematic_Insts.thy index 6d794974b..2170f731d 100644 --- a/lib/Trace_Schematic_Insts.thy +++ b/lib/Trace_Schematic_Insts.thy @@ -7,8 +7,8 @@ theory Trace_Schematic_Insts imports Main - "ml-helpers/MLUtils" - "ml-helpers/TermPatternAntiquote" + MLUtils + TermPatternAntiquote begin text \ diff --git a/lib/Word_Lib/ARM/WordSetup.thy b/lib/Word_Lib/ARM/WordSetup.thy index 3c78a77e2..9f7e29a54 100644 --- a/lib/Word_Lib/ARM/WordSetup.thy +++ b/lib/Word_Lib/ARM/WordSetup.thy @@ -7,8 +7,8 @@ theory WordSetup (* part of non-AFP Word_Lib *) imports - "../Distinct_Prop" - "../Word_Lemmas_32_Internal" + Distinct_Prop + Word_Lemmas_32_Internal begin (* Distinct_Prop lemmas that need word lemmas: *) diff --git a/lib/Word_Lib/ARM_HYP/WordSetup.thy b/lib/Word_Lib/ARM_HYP/WordSetup.thy index 3c78a77e2..9f7e29a54 100644 --- a/lib/Word_Lib/ARM_HYP/WordSetup.thy +++ b/lib/Word_Lib/ARM_HYP/WordSetup.thy @@ -7,8 +7,8 @@ theory WordSetup (* part of non-AFP Word_Lib *) imports - "../Distinct_Prop" - "../Word_Lemmas_32_Internal" + Distinct_Prop + Word_Lemmas_32_Internal begin (* Distinct_Prop lemmas that need word lemmas: *) diff --git a/lib/Word_Lib/RISCV64/WordSetup.thy b/lib/Word_Lib/RISCV64/WordSetup.thy index 16268edc6..204344564 100644 --- a/lib/Word_Lib/RISCV64/WordSetup.thy +++ b/lib/Word_Lib/RISCV64/WordSetup.thy @@ -7,8 +7,8 @@ theory WordSetup (* part of non-AFP Word_Lib *) imports - "../Distinct_Prop" - "../Word_Lemmas_64_Internal" + Distinct_Prop + Word_Lemmas_64_Internal begin (* Distinct_Prop lemmas that need word lemmas: *) diff --git a/lib/Word_Lib/X64/WordSetup.thy b/lib/Word_Lib/X64/WordSetup.thy index 16268edc6..204344564 100644 --- a/lib/Word_Lib/X64/WordSetup.thy +++ b/lib/Word_Lib/X64/WordSetup.thy @@ -7,8 +7,8 @@ theory WordSetup (* part of non-AFP Word_Lib *) imports - "../Distinct_Prop" - "../Word_Lemmas_64_Internal" + Distinct_Prop + Word_Lemmas_64_Internal begin (* Distinct_Prop lemmas that need word lemmas: *) diff --git a/lib/concurrency/examples/Peterson_Atomicity.thy b/lib/concurrency/examples/Peterson_Atomicity.thy index ff96f7bef..2dc98c753 100644 --- a/lib/concurrency/examples/Peterson_Atomicity.thy +++ b/lib/concurrency/examples/Peterson_Atomicity.thy @@ -5,7 +5,7 @@ *) theory Peterson_Atomicity imports - "../Atomicity_Lib" + Atomicity_Lib begin text \ diff --git a/lib/concurrency/examples/Plus2_Prefix.thy b/lib/concurrency/examples/Plus2_Prefix.thy index 53daf0ef3..0e338cb58 100644 --- a/lib/concurrency/examples/Plus2_Prefix.thy +++ b/lib/concurrency/examples/Plus2_Prefix.thy @@ -5,7 +5,7 @@ *) theory Plus2_Prefix imports - "../Prefix_Refinement" + Prefix_Refinement begin section \The plus2 example.\ diff --git a/lib/sep_algebra/ex/Sep_Tactics_Test.thy b/lib/sep_algebra/ex/Sep_Tactics_Test.thy index c0d93d4d2..804722a84 100644 --- a/lib/sep_algebra/ex/Sep_Tactics_Test.thy +++ b/lib/sep_algebra/ex/Sep_Tactics_Test.thy @@ -10,7 +10,7 @@ *) theory Sep_Tactics_Test -imports "../Sep_Tactics" +imports Sep_Tactics begin text \Substitution and forward/backward reasoning\ diff --git a/lib/sep_algebra/ex/Simple_Separation_Example.thy b/lib/sep_algebra/ex/Simple_Separation_Example.thy index b710d7441..2c26b4011 100644 --- a/lib/sep_algebra/ex/Simple_Separation_Example.thy +++ b/lib/sep_algebra/ex/Simple_Separation_Example.thy @@ -15,8 +15,8 @@ chapter "Example from HOL/Hoare/Separation" theory Simple_Separation_Example imports "HOL-Hoare.Hoare_Logic_Abort" - "../Sep_Heap_Instance" - "../Sep_Tactics" + Sep_Heap_Instance + Sep_Tactics begin declare [[syntax_ambiguity_warning = false]] diff --git a/lib/sep_algebra/ex/VM_Example.thy b/lib/sep_algebra/ex/VM_Example.thy index 5a41ab415..99ab42e5d 100644 --- a/lib/sep_algebra/ex/VM_Example.thy +++ b/lib/sep_algebra/ex/VM_Example.thy @@ -14,8 +14,8 @@ chapter "Separation Algebra for Virtual Memory" theory VM_Example imports - "../Sep_Tactics" - "../Map_Extra" + Sep_Tactics + Map_Extra begin text \ diff --git a/lib/sep_algebra/ex/capDL/Abstract_Separation_D.thy b/lib/sep_algebra/ex/capDL/Abstract_Separation_D.thy index 1f35d6da5..5a02fd033 100644 --- a/lib/sep_algebra/ex/capDL/Abstract_Separation_D.thy +++ b/lib/sep_algebra/ex/capDL/Abstract_Separation_D.thy @@ -13,9 +13,9 @@ chapter "Instantiating capDL as a separation algebra." theory Abstract_Separation_D imports - "../../Sep_Tactics" + Sep_Tactics Types_D - "../../Map_Extra" + Map_Extra begin (************************************** diff --git a/proof/crefine/ARM/ArchMove_C.thy b/proof/crefine/ARM/ArchMove_C.thy index ce1d11a0c..1b20850ad 100644 --- a/proof/crefine/ARM/ArchMove_C.thy +++ b/proof/crefine/ARM/ArchMove_C.thy @@ -8,7 +8,7 @@ (* Arch specific lemmas that should be moved into theory files before CRefine *) theory ArchMove_C -imports "../Move_C" +imports Move_C begin lemma ps_clear_is_aligned_ksPSpace_None: diff --git a/proof/crefine/ARM/Ctac_lemmas_C.thy b/proof/crefine/ARM/Ctac_lemmas_C.thy index cbbd964d8..f4a175142 100644 --- a/proof/crefine/ARM/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM/Ctac_lemmas_C.thy @@ -8,7 +8,7 @@ theory Ctac_lemmas_C imports - "../lib/Ctac" + Ctac begin context kernel diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index 1e56a8e91..be269de51 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -7,7 +7,7 @@ chapter "Toplevel Refinement Statement" theory Refine_C -imports Init_C Fastpath_C "../lib/CToCRefine" +imports Init_C Fastpath_C CToCRefine begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy index 00df9c605..bb4733fa2 100644 --- a/proof/crefine/ARM_HYP/ArchMove_C.thy +++ b/proof/crefine/ARM_HYP/ArchMove_C.thy @@ -8,7 +8,7 @@ (* Arch specific lemmas that should be moved into theory files before CRefine *) theory ArchMove_C -imports "../Move_C" +imports Move_C begin (* FIXME move: need a theory on top of CSpec that arches can share *) diff --git a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy index 87a25e688..57283a3f2 100644 --- a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy @@ -8,7 +8,7 @@ theory Ctac_lemmas_C imports - "../lib/Ctac" + Ctac begin context kernel diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index fbb21919a..b3e338220 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -7,7 +7,7 @@ chapter "Toplevel Refinement Statement" theory Refine_C -imports Init_C Fastpath_C "../lib/CToCRefine" +imports Init_C Fastpath_C CToCRefine begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/RISCV64/ArchMove_C.thy b/proof/crefine/RISCV64/ArchMove_C.thy index 2bd7a87ce..9b8670f4d 100644 --- a/proof/crefine/RISCV64/ArchMove_C.thy +++ b/proof/crefine/RISCV64/ArchMove_C.thy @@ -7,7 +7,7 @@ (* Arch specific lemmas that should be moved into theory files before CRefine *) theory ArchMove_C -imports "../Move_C" +imports Move_C begin diff --git a/proof/crefine/RISCV64/Ctac_lemmas_C.thy b/proof/crefine/RISCV64/Ctac_lemmas_C.thy index 6e59357db..97c88a0d6 100644 --- a/proof/crefine/RISCV64/Ctac_lemmas_C.thy +++ b/proof/crefine/RISCV64/Ctac_lemmas_C.thy @@ -8,7 +8,7 @@ theory Ctac_lemmas_C imports - "../lib/Ctac" + Ctac begin context kernel diff --git a/proof/crefine/RISCV64/Refine_C.thy b/proof/crefine/RISCV64/Refine_C.thy index 91c41f125..f244f4d0b 100644 --- a/proof/crefine/RISCV64/Refine_C.thy +++ b/proof/crefine/RISCV64/Refine_C.thy @@ -17,7 +17,7 @@ imports "Refine.RAB_FN" "CLib.MonadicRewrite_C" - "../lib/CToCRefine" + CToCRefine begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/X64/ArchMove_C.thy b/proof/crefine/X64/ArchMove_C.thy index 289fab9f2..bcc2a9e36 100644 --- a/proof/crefine/X64/ArchMove_C.thy +++ b/proof/crefine/X64/ArchMove_C.thy @@ -8,7 +8,7 @@ (* Arch specific lemmas that should be moved into theory files before CRefine *) theory ArchMove_C -imports "../Move_C" +imports Move_C begin lemma ps_clear_is_aligned_ksPSpace_None: diff --git a/proof/crefine/X64/Ctac_lemmas_C.thy b/proof/crefine/X64/Ctac_lemmas_C.thy index f89a9c5a6..9df246cda 100644 --- a/proof/crefine/X64/Ctac_lemmas_C.thy +++ b/proof/crefine/X64/Ctac_lemmas_C.thy @@ -8,7 +8,7 @@ theory Ctac_lemmas_C imports - "../lib/Ctac" + Ctac begin context kernel diff --git a/proof/crefine/X64/Refine_C.thy b/proof/crefine/X64/Refine_C.thy index 705977505..c0fee0251 100644 --- a/proof/crefine/X64/Refine_C.thy +++ b/proof/crefine/X64/Refine_C.thy @@ -17,7 +17,7 @@ imports "Refine.RAB_FN" "CLib.MonadicRewrite_C" - "../lib/CToCRefine" + CToCRefine begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/lib/Corres_C.thy b/proof/crefine/lib/Corres_C.thy index 3198758d6..49ae2eab3 100644 --- a/proof/crefine/lib/Corres_C.thy +++ b/proof/crefine/lib/Corres_C.thy @@ -7,7 +7,7 @@ theory Corres_C imports "CLib.CCorresLemmas" - "../$L4V_ARCH/SR_lemmas_C" + SR_lemmas_C begin abbreviation diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy index 516a7ada2..2a898cbba 100644 --- a/proof/invariant-abstract/ADT_AI.thy +++ b/proof/invariant-abstract/ADT_AI.thy @@ -8,7 +8,7 @@ chapter \Abstract datatype for the abstract specification\ theory ADT_AI imports - "./$L4V_ARCH/ArchADT_AI" + ArchADT_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index aa7480709..68d78248f 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -9,7 +9,7 @@ The main theorem *) theory AInvs -imports "./$L4V_ARCH/ArchAInvsPre" +imports ArchAInvsPre begin lemma st_tcb_at_nostate_upd: diff --git a/proof/invariant-abstract/AInvsPre.thy b/proof/invariant-abstract/AInvsPre.thy index dd447b334..b26d36667 100644 --- a/proof/invariant-abstract/AInvsPre.thy +++ b/proof/invariant-abstract/AInvsPre.thy @@ -5,7 +5,7 @@ *) theory AInvsPre -imports "./$L4V_ARCH/ArchVSpaceEntries_AI" ADT_AI +imports ArchVSpaceEntries_AI ADT_AI begin locale AInvsPre = diff --git a/proof/invariant-abstract/ARM/ArchADT_AI.thy b/proof/invariant-abstract/ARM/ArchADT_AI.thy index b2ad0d8b0..fd177d3ba 100644 --- a/proof/invariant-abstract/ARM/ArchADT_AI.thy +++ b/proof/invariant-abstract/ARM/ArchADT_AI.thy @@ -9,7 +9,7 @@ chapter \ARM-specific definitions for abstract datatype for the abstract s theory ArchADT_AI imports "Lib.Simulation" - "../Invariants_AI" + Invariants_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchAInvsPre.thy b/proof/invariant-abstract/ARM/ArchAInvsPre.thy index 1d1b9a28d..7fb0a57bc 100644 --- a/proof/invariant-abstract/ARM/ArchAInvsPre.thy +++ b/proof/invariant-abstract/ARM/ArchAInvsPre.thy @@ -5,7 +5,7 @@ *) theory ArchAInvsPre -imports "../AInvsPre" +imports AInvsPre begin context Arch begin diff --git a/proof/invariant-abstract/ARM/ArchAcc_AI.thy b/proof/invariant-abstract/ARM/ArchAcc_AI.thy index 608e771d8..c69e0edc5 100644 --- a/proof/invariant-abstract/ARM/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchAcc_AI.thy @@ -9,8 +9,9 @@ Lemmas on arch get/set object etc *) theory ArchAcc_AI -imports "../SubMonad_AI" - "Lib.Crunch_Instances_NonDet" +imports + SubMonad_AI + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy index 5957be89a..c441ba91f 100644 --- a/proof/invariant-abstract/ARM/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy @@ -5,7 +5,7 @@ *) theory ArchArch_AI -imports "../Arch_AI" +imports Arch_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy index d786def87..cafc492f8 100644 --- a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres2_AI imports - "../BCorres2_AI" + BCorres2_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchBCorres_AI.thy b/proof/invariant-abstract/ARM/ArchBCorres_AI.thy index 401942bc6..6e24c680a 100644 --- a/proof/invariant-abstract/ARM/ArchBCorres_AI.thy +++ b/proof/invariant-abstract/ARM/ArchBCorres_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres_AI imports - "../BCorres_AI" + BCorres_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchBits_AI.thy b/proof/invariant-abstract/ARM/ArchBits_AI.thy index dabcf6921..38ce35e87 100644 --- a/proof/invariant-abstract/ARM/ArchBits_AI.thy +++ b/proof/invariant-abstract/ARM/ArchBits_AI.thy @@ -5,7 +5,7 @@ *) theory ArchBits_AI -imports "../Invariants_AI" +imports Invariants_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy b/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy index c00771e1b..9ee0a8f16 100644 --- a/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy @@ -5,7 +5,7 @@ *) theory ArchCNodeInv_AI -imports "../CNodeInv_AI" +imports CNodeInv_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy index 4f4b724e4..a9722c467 100644 --- a/proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpaceInvPre_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInvPre_AI -imports "../CSpaceInvPre_AI" +imports CSpaceInvPre_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy index bbdd3ce7e..15797d43c 100644 --- a/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInv_AI -imports "../CSpaceInv_AI" +imports CSpaceInv_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy b/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy index 64c056250..272d5c233 100644 --- a/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy @@ -9,7 +9,7 @@ ARM-specific CSpace invariants *) theory ArchCSpacePre_AI -imports "../CSpacePre_AI" +imports CSpacePre_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy index 40cc8dd9f..7c90f1c3b 100644 --- a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy @@ -9,7 +9,7 @@ ARM-specific CSpace invariants *) theory ArchCSpace_AI -imports "../CSpace_AI" +imports CSpace_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy index 43cbd4c27..7e89fd30d 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedAux_AI -imports "../DetSchedAux_AI" +imports DetSchedAux_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy index 6941a035b..c0ef7c1d8 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedDomainTime_AI -imports "../DetSchedDomainTime_AI" +imports DetSchedDomainTime_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy index a1b9b65b1..176584884 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedSchedule_AI -imports "../DetSchedSchedule_AI" +imports DetSchedSchedule_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy b/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy index 6d935c639..067625489 100644 --- a/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDeterministic_AI -imports "../Deterministic_AI" +imports Deterministic_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy index ec151900a..a7cfa05fd 100644 --- a/proof/invariant-abstract/ARM/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetype_AI -imports "../Detype_AI" +imports Detype_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy index 75ae2a6ce..c00e5b048 100644 --- a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy @@ -5,7 +5,7 @@ *) theory ArchEmptyFail_AI -imports "../EmptyFail_AI" +imports EmptyFail_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy index a2ae7b6ec..251d17922 100644 --- a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy @@ -5,7 +5,7 @@ *) theory ArchFinalise_AI -imports "../Finalise_AI" +imports Finalise_AI begin context Arch begin diff --git a/proof/invariant-abstract/ARM/ArchInterruptAcc_AI.thy b/proof/invariant-abstract/ARM/ArchInterruptAcc_AI.thy index b88b9066d..2f863b1c1 100644 --- a/proof/invariant-abstract/ARM/ArchInterruptAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterruptAcc_AI.thy @@ -9,7 +9,7 @@ *) theory ArchInterruptAcc_AI -imports "../InterruptAcc_AI" +imports InterruptAcc_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy index 9036e50f5..315e9aec2 100644 --- a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInterrupt_AI -imports "../Interrupt_AI" +imports Interrupt_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy index 2ee991079..6d6a64840 100644 --- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInvariants_AI -imports "../InvariantsPre_AI" +imports InvariantsPre_AI begin \ \---------------------------------------------------------------------------\ diff --git a/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy b/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy index f8abc5af8..7176e6c6b 100644 --- a/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpcCancel_AI -imports "../IpcCancel_AI" +imports IpcCancel_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy index 60f608f93..c08d73acb 100644 --- a/proof/invariant-abstract/ARM/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpc_AI -imports "../Ipc_AI" +imports Ipc_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy index ea4884022..d631f3c94 100644 --- a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy @@ -5,7 +5,7 @@ *) theory ArchKHeap_AI -imports "../KHeapPre_AI" +imports KHeapPre_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy b/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy index b5009c16b..40616cd0d 100644 --- a/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy @@ -9,9 +9,9 @@ theory ArchKernelInit_AI imports - "../ADT_AI" - "../Tcb_AI" - "../Arch_AI" + ADT_AI + Tcb_AI + Arch_AI begin context Arch begin global_naming ARM (*FIXME: arch_split*) diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy index 1831c54bd..65372f0be 100644 --- a/proof/invariant-abstract/ARM/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -9,7 +9,7 @@ *) theory ArchRetype_AI -imports "../Retype_AI" +imports Retype_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy index fd6a0871a..bcc60b324 100644 --- a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchSchedule_AI -imports "../Schedule_AI" +imports Schedule_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchSyscall_AI.thy b/proof/invariant-abstract/ARM/ArchSyscall_AI.thy index 01cd026b4..f9ec2313d 100644 --- a/proof/invariant-abstract/ARM/ArchSyscall_AI.thy +++ b/proof/invariant-abstract/ARM/ArchSyscall_AI.thy @@ -10,7 +10,7 @@ Refinement for handleEvent and syscalls theory ArchSyscall_AI imports - "../Syscall_AI" + Syscall_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchTcbAcc_AI.thy b/proof/invariant-abstract/ARM/ArchTcbAcc_AI.thy index ee0521fd1..d3a13b359 100644 --- a/proof/invariant-abstract/ARM/ArchTcbAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcbAcc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcbAcc_AI -imports "../TcbAcc_AI" +imports TcbAcc_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index c4ea3db0a..77e2c0c6f 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcb_AI -imports "../Tcb_AI" +imports Tcb_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy index 792fac114..8ad8c6d5e 100644 --- a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -5,7 +5,7 @@ *) theory ArchUntyped_AI -imports "../Untyped_AI" +imports Untyped_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index 657f0b0d3..1327c3424 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -5,7 +5,7 @@ *) theory ArchVSpaceEntries_AI -imports "../VSpaceEntries_AI" +imports VSpaceEntries_AI begin diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index 54633d3f5..be869be49 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -9,7 +9,7 @@ ARM-specific VSpace invariants *) theory ArchVSpace_AI -imports "../VSpacePre_AI" +imports VSpacePre_AI begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/Machine_AI.thy b/proof/invariant-abstract/ARM/Machine_AI.thy index b86b53cd0..68e817a9f 100644 --- a/proof/invariant-abstract/ARM/Machine_AI.thy +++ b/proof/invariant-abstract/ARM/Machine_AI.thy @@ -9,7 +9,7 @@ Properties of machine operations. *) theory Machine_AI -imports "../Bits_AI" +imports Bits_AI begin diff --git a/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy index 844d6f36f..d29d2eb0d 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy @@ -9,7 +9,7 @@ chapter \ARM_HYP-specific definitions for abstract datatype for the abstra theory ArchADT_AI imports "Lib.Simulation" - "../Invariants_AI" + Invariants_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy b/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy index b0d5a67ec..8463c6f2d 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy @@ -5,7 +5,7 @@ *) theory ArchAInvsPre -imports "../AInvsPre" +imports AInvsPre begin context Arch begin diff --git a/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy index 81118d091..9733cf9d1 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy @@ -9,8 +9,9 @@ Lemmas on arch get/set object etc *) theory ArchAcc_AI -imports "../SubMonad_AI" - "Lib.Crunch_Instances_NonDet" +imports + SubMonad_AI + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy index cf0bf9704..22f2aee69 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy @@ -5,7 +5,7 @@ *) theory ArchArch_AI -imports "../Arch_AI" +imports Arch_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy index 2238b4bef..fd15d996a 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchBCorres2_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres2_AI imports - "../BCorres2_AI" + BCorres2_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchBCorres_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchBCorres_AI.thy index 0407aa543..a5754a44c 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchBCorres_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchBCorres_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres_AI imports - "../BCorres_AI" + BCorres_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchBits_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchBits_AI.thy index 1bc9f2bb9..90c2ff8dd 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchBits_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchBits_AI.thy @@ -5,7 +5,7 @@ *) theory ArchBits_AI -imports "../Invariants_AI" +imports Invariants_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy index 16fe8ed84..38faafe7c 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy @@ -5,7 +5,7 @@ *) theory ArchCNodeInv_AI -imports "../CNodeInv_AI" +imports CNodeInv_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy index d9f56c89c..b41b447db 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInvPre_AI -imports "../CSpaceInvPre_AI" +imports CSpaceInvPre_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCSpaceInv_AI.thy index 0dc33dcd0..0b4540ef1 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchCSpaceInv_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchCSpaceInv_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInv_AI -imports "../CSpaceInv_AI" +imports CSpaceInv_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchCSpacePre_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCSpacePre_AI.thy index 8c15a8f37..019f1d3e3 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchCSpacePre_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchCSpacePre_AI.thy @@ -9,7 +9,7 @@ ARM_HYP-specific CSpace invariants *) theory ArchCSpacePre_AI -imports "../CSpacePre_AI" +imports CSpacePre_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy index 213d256f1..11a9b0fa2 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchCSpace_AI.thy @@ -9,7 +9,7 @@ ARM_HYP-specific CSpace invariants *) theory ArchCSpace_AI -imports "../CSpace_AI" +imports CSpace_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetSchedAux_AI.thy index b23457fdc..68bc4bc64 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetSchedAux_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedAux_AI -imports "../DetSchedAux_AI" +imports DetSchedAux_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetSchedDomainTime_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetSchedDomainTime_AI.thy index 7c598d135..cce9c4f7d 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetSchedDomainTime_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedDomainTime_AI -imports "../DetSchedDomainTime_AI" +imports DetSchedDomainTime_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy index 14f010190..7f1085734 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedSchedule_AI -imports "../DetSchedSchedule_AI" +imports DetSchedSchedule_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchDeterministic_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDeterministic_AI.thy index d33203fe8..75a25b13b 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDeterministic_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDeterministic_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDeterministic_AI -imports "../Deterministic_AI" +imports Deterministic_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy index 9132c1d49..51e176dff 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetype_AI -imports "../Detype_AI" +imports Detype_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy index b94ee4611..00ffe2742 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy @@ -5,7 +5,7 @@ *) theory ArchEmptyFail_AI -imports "../EmptyFail_AI" +imports EmptyFail_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy index 409bb045a..4ed7be37b 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy @@ -5,7 +5,7 @@ *) theory ArchFinalise_AI -imports "../Finalise_AI" +imports Finalise_AI begin context Arch begin diff --git a/proof/invariant-abstract/ARM_HYP/ArchInterruptAcc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInterruptAcc_AI.thy index 33d148aa7..9581a0b65 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchInterruptAcc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchInterruptAcc_AI.thy @@ -9,7 +9,7 @@ *) theory ArchInterruptAcc_AI -imports "../InterruptAcc_AI" +imports InterruptAcc_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy index 2fdc7d6f0..27073e94e 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInterrupt_AI -imports "../Interrupt_AI" +imports Interrupt_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy index 5d56ddea4..834c434a4 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInvariants_AI -imports "../InvariantsPre_AI" +imports InvariantsPre_AI begin \ \---------------------------------------------------------------------------\ diff --git a/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy index 18444216c..2ead3ca54 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpcCancel_AI -imports "../IpcCancel_AI" +imports IpcCancel_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy index 6e7433419..c38b48cf2 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpc_AI -imports "../Ipc_AI" +imports Ipc_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy index 832f52f69..0f5e04034 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy @@ -5,7 +5,7 @@ *) theory ArchKHeap_AI -imports "../KHeapPre_AI" +imports KHeapPre_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy index 456b4614d..ebecde71b 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy @@ -9,9 +9,9 @@ theory ArchKernelInit_AI imports - "../ADT_AI" - "../Tcb_AI" - "../Arch_AI" + ADT_AI + Tcb_AI + Arch_AI begin context Arch begin global_naming ARM (*FIXME: arch_split*) diff --git a/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy index ed62d1361..899ff568a 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy @@ -9,7 +9,7 @@ *) theory ArchRetype_AI -imports "../Retype_AI" +imports Retype_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy index 012126831..27b916ce1 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchSchedule_AI -imports "../Schedule_AI" +imports Schedule_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchSyscall_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchSyscall_AI.thy index 274cbcd42..1e4864b99 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchSyscall_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchSyscall_AI.thy @@ -10,7 +10,7 @@ Refinement for handleEvent and syscalls theory ArchSyscall_AI imports - "../Syscall_AI" + Syscall_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchTcbAcc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchTcbAcc_AI.thy index 158425425..96a31de24 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchTcbAcc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchTcbAcc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcbAcc_AI -imports "../TcbAcc_AI" +imports TcbAcc_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy index 9993298a3..b303018fe 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcb_AI -imports "../Tcb_AI" +imports Tcb_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy index 61bcb4e9d..612c98a91 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy @@ -5,7 +5,7 @@ *) theory ArchUntyped_AI -imports "../Untyped_AI" +imports Untyped_AI begin context Arch begin global_naming ARM_HYP diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy index 7f81d7df4..612e00178 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy @@ -5,7 +5,7 @@ *) theory ArchVSpaceEntries_AI -imports "../VSpaceEntries_AI" +imports VSpaceEntries_AI begin context Arch begin global_naming ARM_HYP (*FIXME: arch_split*) diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy index b4990ec28..401bef0b6 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy @@ -9,7 +9,7 @@ ARM_HYP-specific VSpace invariants *) theory ArchVSpace_AI -imports "../VSpacePre_AI" +imports VSpacePre_AI begin (* FIXME: move *) diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy index d580d64e4..175f37708 100644 --- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy @@ -9,7 +9,7 @@ Properties of machine operations. *) theory Machine_AI -imports "../Bits_AI" +imports Bits_AI begin diff --git a/proof/invariant-abstract/Arch_AI.thy b/proof/invariant-abstract/Arch_AI.thy index e904e12ba..e3118ddd0 100644 --- a/proof/invariant-abstract/Arch_AI.thy +++ b/proof/invariant-abstract/Arch_AI.thy @@ -9,7 +9,7 @@ Top level architecture related proofs. *) theory Arch_AI -imports "./$L4V_ARCH/ArchUntyped_AI" "./$L4V_ARCH/ArchFinalise_AI" +imports ArchUntyped_AI ArchFinalise_AI begin declare detype_arch_state[simp] diff --git a/proof/invariant-abstract/BCorres2_AI.thy b/proof/invariant-abstract/BCorres2_AI.thy index 958e6e54b..66cd617b5 100644 --- a/proof/invariant-abstract/BCorres2_AI.thy +++ b/proof/invariant-abstract/BCorres2_AI.thy @@ -6,7 +6,7 @@ theory BCorres2_AI imports - "./$L4V_ARCH/ArchEmptyFail_AI" + ArchEmptyFail_AI begin locale BCorres2_AI = diff --git a/proof/invariant-abstract/Bits_AI.thy b/proof/invariant-abstract/Bits_AI.thy index 36c45f544..06da5d09f 100644 --- a/proof/invariant-abstract/Bits_AI.thy +++ b/proof/invariant-abstract/Bits_AI.thy @@ -5,7 +5,7 @@ *) theory Bits_AI -imports "./$L4V_ARCH/ArchBits_AI" +imports ArchBits_AI begin lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp' diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index 1e5ccbe82..a91296535 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -10,7 +10,7 @@ recursive revoke and delete operations. *) theory CNodeInv_AI -imports "./$L4V_ARCH/ArchIpc_AI" +imports ArchIpc_AI begin diff --git a/proof/invariant-abstract/CSpaceInvPre_AI.thy b/proof/invariant-abstract/CSpaceInvPre_AI.thy index 71f20c009..a9ddda626 100644 --- a/proof/invariant-abstract/CSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/CSpaceInvPre_AI.thy @@ -5,7 +5,7 @@ *) theory CSpaceInvPre_AI -imports "./$L4V_ARCH/ArchAcc_AI" +imports ArchAcc_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index dac1b9b03..611f25f5d 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory CSpaceInv_AI -imports "./$L4V_ARCH/ArchCSpaceInvPre_AI" +imports ArchCSpaceInvPre_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/CSpacePre_AI.thy b/proof/invariant-abstract/CSpacePre_AI.thy index bd7be7fd1..f94098cb0 100644 --- a/proof/invariant-abstract/CSpacePre_AI.thy +++ b/proof/invariant-abstract/CSpacePre_AI.thy @@ -9,7 +9,7 @@ CSpace invariants preamble *) theory CSpacePre_AI -imports "./$L4V_ARCH/ArchCSpaceInv_AI" +imports ArchCSpaceInv_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index fc6f550fc..7775f96a7 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -9,7 +9,7 @@ CSpace refinement *) theory CSpace_AI -imports "./$L4V_ARCH/ArchCSpacePre_AI" +imports ArchCSpacePre_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/DetSchedDomainTime_AI.thy b/proof/invariant-abstract/DetSchedDomainTime_AI.thy index 03561521b..4f56a5489 100644 --- a/proof/invariant-abstract/DetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/DetSchedDomainTime_AI.thy @@ -5,7 +5,7 @@ *) theory DetSchedDomainTime_AI -imports "$L4V_ARCH/ArchDetSchedAux_AI" +imports ArchDetSchedAux_AI begin text \ diff --git a/proof/invariant-abstract/DetSchedInvs_AI.thy b/proof/invariant-abstract/DetSchedInvs_AI.thy index 61c8d6ed6..caa43d9f6 100644 --- a/proof/invariant-abstract/DetSchedInvs_AI.thy +++ b/proof/invariant-abstract/DetSchedInvs_AI.thy @@ -5,7 +5,7 @@ *) theory DetSchedInvs_AI -imports "$L4V_ARCH/ArchDeterministic_AI" +imports ArchDeterministic_AI begin lemma get_etcb_rev: diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index f7620a08e..775e164c6 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory DetSchedSchedule_AI -imports "$L4V_ARCH/ArchDetSchedDomainTime_AI" +imports ArchDetSchedDomainTime_AI begin crunch ct_not_in_q[wp]: do_machine_op "ct_not_in_q" diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index 0b0a0b1ce..e373d12b5 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -5,7 +5,7 @@ *) theory Detype_AI -imports "./$L4V_ARCH/ArchRetype_AI" +imports ArchRetype_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy index 2361644d7..526697bd9 100644 --- a/proof/invariant-abstract/EmptyFail_AI.thy +++ b/proof/invariant-abstract/EmptyFail_AI.thy @@ -5,7 +5,7 @@ *) theory EmptyFail_AI -imports "./$L4V_ARCH/ArchTcb_AI" +imports ArchTcb_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 50c960969..00a643925 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -6,9 +6,9 @@ theory Finalise_AI imports - "./$L4V_ARCH/ArchIpcCancel_AI" - "./$L4V_ARCH/ArchInterruptAcc_AI" - "./$L4V_ARCH/ArchRetype_AI" + ArchIpcCancel_AI + ArchInterruptAcc_AI + ArchRetype_AI begin definition diff --git a/proof/invariant-abstract/Include_AI.thy b/proof/invariant-abstract/Include_AI.thy index b6be6de30..ce19ce242 100644 --- a/proof/invariant-abstract/Include_AI.thy +++ b/proof/invariant-abstract/Include_AI.thy @@ -6,7 +6,7 @@ theory Include_AI imports - "./$L4V_ARCH/ArchCrunchSetup_AI" + ArchCrunchSetup_AI "Lib.Eisbach_WP" "ASpec.Syscall_A" "Lib.LemmaBucket" diff --git a/proof/invariant-abstract/InterruptAcc_AI.thy b/proof/invariant-abstract/InterruptAcc_AI.thy index da6f6d402..b05b8f8b3 100644 --- a/proof/invariant-abstract/InterruptAcc_AI.thy +++ b/proof/invariant-abstract/InterruptAcc_AI.thy @@ -6,7 +6,7 @@ theory InterruptAcc_AI -imports "$L4V_ARCH/ArchTcbAcc_AI" +imports ArchTcbAcc_AI begin lemma get_irq_slot_real_cte[wp]: diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index 973e761f7..bf1714696 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -9,7 +9,7 @@ Refinement for interrupt controller operations *) theory Interrupt_AI -imports "./$L4V_ARCH/ArchIpc_AI" +imports ArchIpc_AI begin diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 4ee4ce015..8bb0ff4a3 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -5,7 +5,7 @@ *) theory Invariants_AI -imports "./$L4V_ARCH/ArchInvariants_AI" +imports ArchInvariants_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 3c6bf58f4..3d04c7260 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -5,7 +5,7 @@ *) theory IpcCancel_AI -imports "./$L4V_ARCH/ArchSchedule_AI" +imports ArchSchedule_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index 9807682cb..32ee891d9 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -5,7 +5,8 @@ *) theory Ipc_AI -imports "./$L4V_ARCH/ArchFinalise_AI" +imports + ArchFinalise_AI "Lib.WPBang" begin diff --git a/proof/invariant-abstract/KHeapPre_AI.thy b/proof/invariant-abstract/KHeapPre_AI.thy index 043bfb154..14f9b8589 100644 --- a/proof/invariant-abstract/KHeapPre_AI.thy +++ b/proof/invariant-abstract/KHeapPre_AI.thy @@ -5,7 +5,7 @@ *) theory KHeapPre_AI -imports "./$L4V_ARCH/Machine_AI" +imports Machine_AI begin primrec diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index acebf3da3..e91041ca7 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -5,7 +5,7 @@ *) theory KHeap_AI -imports "./$L4V_ARCH/ArchKHeap_AI" +imports ArchKHeap_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/KernelInit_AI.thy b/proof/invariant-abstract/KernelInit_AI.thy index f2756aa38..7b31fa5ae 100644 --- a/proof/invariant-abstract/KernelInit_AI.thy +++ b/proof/invariant-abstract/KernelInit_AI.thy @@ -9,7 +9,7 @@ theory KernelInit_AI imports - "./$L4V_ARCH/ArchKernelInit_AI" + ArchKernelInit_AI begin axiomatization where diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index 082cf8bc1..ca64df840 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -6,7 +6,7 @@ theory LevityCatch_AI imports - "./$L4V_ARCH/ArchLevityCatch_AI" + ArchLevityCatch_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/RISCV64/ArchADT_AI.thy b/proof/invariant-abstract/RISCV64/ArchADT_AI.thy index 7a3ba9b97..17c4ce466 100644 --- a/proof/invariant-abstract/RISCV64/ArchADT_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchADT_AI.thy @@ -9,7 +9,7 @@ chapter \RISCV64-specific definitions for abstract datatype for the abstra theory ArchADT_AI imports "Lib.Simulation" - "../Invariants_AI" + Invariants_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy b/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy index c968ee147..eae55f242 100644 --- a/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy +++ b/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy @@ -5,7 +5,7 @@ *) theory ArchAInvsPre -imports "../AInvsPre" +imports AInvsPre begin context Arch begin diff --git a/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy b/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy index afc615d26..20402974c 100644 --- a/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchAcc_AI.thy @@ -9,7 +9,7 @@ Lemmas on arch get/set object etc *) theory ArchAcc_AI -imports "../SubMonad_AI" "Lib.Crunch_Instances_NonDet" +imports SubMonad_AI "Lib.Crunch_Instances_NonDet" begin context non_vspace_op diff --git a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy index c253981e6..25e851493 100644 --- a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy @@ -5,7 +5,7 @@ *) theory ArchArch_AI -imports "../Arch_AI" +imports Arch_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchBCorres2_AI.thy b/proof/invariant-abstract/RISCV64/ArchBCorres2_AI.thy index 984a10408..1920f5416 100644 --- a/proof/invariant-abstract/RISCV64/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchBCorres2_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres2_AI imports - "../BCorres2_AI" + BCorres2_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchBCorres_AI.thy b/proof/invariant-abstract/RISCV64/ArchBCorres_AI.thy index d3054b17d..ec18df7d3 100644 --- a/proof/invariant-abstract/RISCV64/ArchBCorres_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchBCorres_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres_AI imports - "../BCorres_AI" + BCorres_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchBits_AI.thy b/proof/invariant-abstract/RISCV64/ArchBits_AI.thy index a7c2f15e4..f5064287e 100644 --- a/proof/invariant-abstract/RISCV64/ArchBits_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchBits_AI.thy @@ -5,7 +5,7 @@ *) theory ArchBits_AI -imports "../Invariants_AI" +imports Invariants_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/RISCV64/ArchCNodeInv_AI.thy index 9610beace..924b1682b 100644 --- a/proof/invariant-abstract/RISCV64/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchCNodeInv_AI.thy @@ -5,7 +5,7 @@ *) theory ArchCNodeInv_AI -imports "../CNodeInv_AI" +imports CNodeInv_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy index b5e19a7a6..eada02b44 100644 --- a/proof/invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchCSpaceInvPre_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInvPre_AI -imports "../CSpaceInvPre_AI" +imports CSpaceInvPre_AI begin diff --git a/proof/invariant-abstract/RISCV64/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/RISCV64/ArchCSpaceInv_AI.thy index 2ad81640b..4f0db7352 100644 --- a/proof/invariant-abstract/RISCV64/ArchCSpaceInv_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchCSpaceInv_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInv_AI -imports "../CSpaceInv_AI" +imports CSpaceInv_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchCSpacePre_AI.thy b/proof/invariant-abstract/RISCV64/ArchCSpacePre_AI.thy index 60986972c..168c983d2 100644 --- a/proof/invariant-abstract/RISCV64/ArchCSpacePre_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchCSpacePre_AI.thy @@ -9,7 +9,7 @@ RISCV64-specific CSpace invariants *) theory ArchCSpacePre_AI -imports "../CSpacePre_AI" +imports CSpacePre_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy b/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy index 98e0b3325..58b5c5850 100644 --- a/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy @@ -9,7 +9,7 @@ Architecture-specific CSpace invariants *) theory ArchCSpace_AI -imports "../CSpace_AI" +imports CSpace_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy index e33826506..222801764 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedAux_AI -imports "../DetSchedAux_AI" +imports DetSchedAux_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedDomainTime_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedDomainTime_AI.thy index c7f9442e8..583b9b312 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetSchedDomainTime_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedDomainTime_AI -imports "../DetSchedDomainTime_AI" +imports DetSchedDomainTime_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy index 7657da1ea..fc881ee93 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedSchedule_AI -imports "../DetSchedSchedule_AI" +imports DetSchedSchedule_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchDeterministic_AI.thy b/proof/invariant-abstract/RISCV64/ArchDeterministic_AI.thy index 18ff0ba48..88fbd0fca 100644 --- a/proof/invariant-abstract/RISCV64/ArchDeterministic_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDeterministic_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDeterministic_AI -imports "../Deterministic_AI" +imports Deterministic_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy index 9323c7dbc..6d59f7ec0 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetype_AI -imports "../Detype_AI" +imports Detype_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy index ca4edab73..68d56ab95 100644 --- a/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy @@ -5,7 +5,7 @@ *) theory ArchEmptyFail_AI -imports "../EmptyFail_AI" +imports EmptyFail_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy index e4495ff47..4d3a316a3 100644 --- a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy @@ -5,7 +5,7 @@ *) theory ArchFinalise_AI -imports "../Finalise_AI" +imports Finalise_AI begin (* FIXME: MOVE *) diff --git a/proof/invariant-abstract/RISCV64/ArchInterruptAcc_AI.thy b/proof/invariant-abstract/RISCV64/ArchInterruptAcc_AI.thy index cd41dbc3c..fe7bf763d 100644 --- a/proof/invariant-abstract/RISCV64/ArchInterruptAcc_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInterruptAcc_AI.thy @@ -9,7 +9,7 @@ *) theory ArchInterruptAcc_AI -imports "../InterruptAcc_AI" +imports InterruptAcc_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy index 012bcf14d..7ad991a62 100644 --- a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInterrupt_AI -imports "../Interrupt_AI" +imports Interrupt_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy b/proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy index ae39346d2..3c7182d27 100644 --- a/proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInvariants_AI -imports "../InvariantsPre_AI" "Lib.Apply_Trace_Cmd" +imports InvariantsPre_AI "Lib.Apply_Trace_Cmd" begin (* setup *) diff --git a/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy b/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy index c8924632d..0437e60b5 100644 --- a/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpcCancel_AI -imports "../IpcCancel_AI" +imports IpcCancel_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy b/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy index e9f736454..f0e3e43bc 100644 --- a/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpc_AI -imports "../Ipc_AI" +imports Ipc_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy b/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy index de503bc12..2a0ddb884 100644 --- a/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy @@ -5,7 +5,7 @@ *) theory ArchKHeap_AI -imports "../KHeapPre_AI" +imports KHeapPre_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy b/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy index dc01fcbc0..8bd08ac82 100644 --- a/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy @@ -6,9 +6,9 @@ theory ArchKernelInit_AI imports - "../ADT_AI" - "../Tcb_AI" - "../Arch_AI" + ADT_AI + Tcb_AI + Arch_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy b/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy index c531ccc55..2ae38af59 100644 --- a/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy @@ -9,7 +9,7 @@ *) theory ArchRetype_AI -imports "../Retype_AI" +imports Retype_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy b/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy index a889611b8..71108ca98 100644 --- a/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchSchedule_AI -imports "../Schedule_AI" +imports Schedule_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchSyscall_AI.thy b/proof/invariant-abstract/RISCV64/ArchSyscall_AI.thy index 1d274174e..73096dfc0 100644 --- a/proof/invariant-abstract/RISCV64/ArchSyscall_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchSyscall_AI.thy @@ -10,7 +10,7 @@ Refinement for handleEvent and syscalls theory ArchSyscall_AI imports - "../Syscall_AI" + Syscall_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchTcbAcc_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcbAcc_AI.thy index 4b4b5a39e..0eaa79471 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcbAcc_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcbAcc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcbAcc_AI -imports "../TcbAcc_AI" +imports TcbAcc_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index 14bc164f4..f2f28a178 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcb_AI -imports "../Tcb_AI" +imports Tcb_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy b/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy index 05fe5c6b6..8d4c55f6b 100644 --- a/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy @@ -5,7 +5,7 @@ *) theory ArchUntyped_AI -imports "../Untyped_AI" +imports Untyped_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy index 6078f8003..3abb8fa67 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy @@ -5,7 +5,7 @@ *) theory ArchVSpaceEntries_AI -imports "../VSpaceEntries_AI" +imports VSpaceEntries_AI begin context Arch begin global_naming RISCV64 diff --git a/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy index a56a7208a..53154a6b8 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpace_AI.thy @@ -9,7 +9,7 @@ RISCV-specific VSpace invariants *) theory ArchVSpace_AI -imports "../VSpacePre_AI" +imports VSpacePre_AI begin (* FIXME: move to lib *) diff --git a/proof/invariant-abstract/RISCV64/Machine_AI.thy b/proof/invariant-abstract/RISCV64/Machine_AI.thy index e5a85ea61..6aa566083 100644 --- a/proof/invariant-abstract/RISCV64/Machine_AI.thy +++ b/proof/invariant-abstract/RISCV64/Machine_AI.thy @@ -9,7 +9,7 @@ Properties of machine operations. *) theory Machine_AI -imports "../Bits_AI" +imports Bits_AI begin diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index c113fd263..a0547d4fe 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -10,10 +10,10 @@ Invariant preservation for all syscalls. theory Syscall_AI imports - "./$L4V_ARCH/ArchBCorres2_AI" - "./$L4V_ARCH/ArchTcb_AI" - "./$L4V_ARCH/ArchArch_AI" - "./$L4V_ARCH/ArchInterrupt_AI" + ArchBCorres2_AI + ArchTcb_AI + ArchArch_AI + ArchInterrupt_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy index dcec799f1..bc5344f9c 100644 --- a/proof/invariant-abstract/TcbAcc_AI.thy +++ b/proof/invariant-abstract/TcbAcc_AI.thy @@ -5,7 +5,7 @@ *) theory TcbAcc_AI -imports "$L4V_ARCH/ArchCSpace_AI" +imports ArchCSpace_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 9d35b0fed..b0f015089 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -5,7 +5,7 @@ *) theory Tcb_AI -imports "./$L4V_ARCH/ArchCNodeInv_AI" +imports ArchCNodeInv_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index 0af6583dd..7002388e4 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -7,7 +7,8 @@ (* Proofs about untyped invocations. *) theory Untyped_AI -imports "./$L4V_ARCH/ArchDetype_AI" +imports + ArchDetype_AI "Lib.MonadicRewrite" begin diff --git a/proof/invariant-abstract/VSpaceEntries_AI.thy b/proof/invariant-abstract/VSpaceEntries_AI.thy index d25cf6c46..65916c31c 100644 --- a/proof/invariant-abstract/VSpaceEntries_AI.thy +++ b/proof/invariant-abstract/VSpaceEntries_AI.thy @@ -5,7 +5,7 @@ *) theory VSpaceEntries_AI -imports "./$L4V_ARCH/ArchSyscall_AI" +imports ArchSyscall_AI begin definition valid_entries :: " ('b \ ('a::len) word \ 'c set) \ (('a::len) word \ 'b) \ bool" diff --git a/proof/invariant-abstract/VSpacePre_AI.thy b/proof/invariant-abstract/VSpacePre_AI.thy index 4486a3dfb..b59ab3a7b 100644 --- a/proof/invariant-abstract/VSpacePre_AI.thy +++ b/proof/invariant-abstract/VSpacePre_AI.thy @@ -9,7 +9,7 @@ VSpace refinement *) theory VSpacePre_AI -imports "$L4V_ARCH/ArchTcbAcc_AI" +imports ArchTcbAcc_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/VSpace_AI.thy b/proof/invariant-abstract/VSpace_AI.thy index 48937b00a..29fd74b1a 100644 --- a/proof/invariant-abstract/VSpace_AI.thy +++ b/proof/invariant-abstract/VSpace_AI.thy @@ -9,7 +9,7 @@ Architecture-independent VSpace invariant proofs *) theory VSpace_AI -imports "./$L4V_ARCH/ArchVSpace_AI" +imports ArchVSpace_AI begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/X64/ArchADT_AI.thy b/proof/invariant-abstract/X64/ArchADT_AI.thy index bb43ee730..858bcd24b 100644 --- a/proof/invariant-abstract/X64/ArchADT_AI.thy +++ b/proof/invariant-abstract/X64/ArchADT_AI.thy @@ -9,7 +9,7 @@ chapter \X64-specific definitions for abstract datatype for the abstract s theory ArchADT_AI imports "Lib.Simulation" - "../Invariants_AI" + Invariants_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchAInvsPre.thy b/proof/invariant-abstract/X64/ArchAInvsPre.thy index 3143f2393..f345647dd 100644 --- a/proof/invariant-abstract/X64/ArchAInvsPre.thy +++ b/proof/invariant-abstract/X64/ArchAInvsPre.thy @@ -5,7 +5,7 @@ *) theory ArchAInvsPre -imports "../AInvsPre" +imports AInvsPre begin context Arch begin diff --git a/proof/invariant-abstract/X64/ArchAcc_AI.thy b/proof/invariant-abstract/X64/ArchAcc_AI.thy index 6223a97d5..82cff21a1 100644 --- a/proof/invariant-abstract/X64/ArchAcc_AI.thy +++ b/proof/invariant-abstract/X64/ArchAcc_AI.thy @@ -9,7 +9,8 @@ Lemmas on arch get/set object etc *) theory ArchAcc_AI -imports "../SubMonad_AI" "ArchVSpaceLookup_AI" "Lib.Crunch_Instances_NonDet" +imports + SubMonad_AI ArchVSpaceLookup_AI "Lib.Crunch_Instances_NonDet" begin diff --git a/proof/invariant-abstract/X64/ArchArch_AI.thy b/proof/invariant-abstract/X64/ArchArch_AI.thy index 2dc5781e1..1ccb0a260 100644 --- a/proof/invariant-abstract/X64/ArchArch_AI.thy +++ b/proof/invariant-abstract/X64/ArchArch_AI.thy @@ -5,7 +5,7 @@ *) theory ArchArch_AI -imports "../Arch_AI" +imports Arch_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchBCorres2_AI.thy b/proof/invariant-abstract/X64/ArchBCorres2_AI.thy index 27d6a5fb2..1d4fc8fec 100644 --- a/proof/invariant-abstract/X64/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/X64/ArchBCorres2_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres2_AI imports - "../BCorres2_AI" + BCorres2_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchBCorres_AI.thy b/proof/invariant-abstract/X64/ArchBCorres_AI.thy index 721f6df3d..00121fb41 100644 --- a/proof/invariant-abstract/X64/ArchBCorres_AI.thy +++ b/proof/invariant-abstract/X64/ArchBCorres_AI.thy @@ -6,7 +6,7 @@ theory ArchBCorres_AI imports - "../BCorres_AI" + BCorres_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchBits_AI.thy b/proof/invariant-abstract/X64/ArchBits_AI.thy index 76f6fb90d..357f3b095 100644 --- a/proof/invariant-abstract/X64/ArchBits_AI.thy +++ b/proof/invariant-abstract/X64/ArchBits_AI.thy @@ -5,7 +5,7 @@ *) theory ArchBits_AI -imports "../Invariants_AI" +imports Invariants_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy index 111a3a2c3..65b1afba2 100644 --- a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy @@ -5,7 +5,7 @@ *) theory ArchCNodeInv_AI -imports "../CNodeInv_AI" +imports CNodeInv_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy index e71a0b627..92c677bb6 100644 --- a/proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInvPre_AI -imports "../CSpaceInvPre_AI" +imports CSpaceInvPre_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy index 48b9e8877..ae304f05e 100644 --- a/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy +++ b/proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy @@ -9,7 +9,7 @@ CSpace invariants *) theory ArchCSpaceInv_AI -imports "../CSpaceInv_AI" +imports CSpaceInv_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchCSpacePre_AI.thy b/proof/invariant-abstract/X64/ArchCSpacePre_AI.thy index 48aa2aa5d..afd13acba 100644 --- a/proof/invariant-abstract/X64/ArchCSpacePre_AI.thy +++ b/proof/invariant-abstract/X64/ArchCSpacePre_AI.thy @@ -9,7 +9,7 @@ X64-specific CSpace invariants *) theory ArchCSpacePre_AI -imports "../CSpacePre_AI" +imports CSpacePre_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchCSpace_AI.thy b/proof/invariant-abstract/X64/ArchCSpace_AI.thy index 7d78911ea..117bb2c81 100644 --- a/proof/invariant-abstract/X64/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/X64/ArchCSpace_AI.thy @@ -9,7 +9,7 @@ X64-specific CSpace invariants *) theory ArchCSpace_AI -imports "../CSpace_AI" +imports CSpace_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy index 56a10a54b..497342c21 100644 --- a/proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedAux_AI -imports "../DetSchedAux_AI" +imports DetSchedAux_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchDetSchedDomainTime_AI.thy b/proof/invariant-abstract/X64/ArchDetSchedDomainTime_AI.thy index cad951b8d..3285d41a5 100644 --- a/proof/invariant-abstract/X64/ArchDetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetSchedDomainTime_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedDomainTime_AI -imports "../DetSchedDomainTime_AI" +imports DetSchedDomainTime_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy index c966ad78e..41f4d78ea 100644 --- a/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetSchedSchedule_AI -imports "../DetSchedSchedule_AI" +imports DetSchedSchedule_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchDeterministic_AI.thy b/proof/invariant-abstract/X64/ArchDeterministic_AI.thy index a59114de6..9289d23fe 100644 --- a/proof/invariant-abstract/X64/ArchDeterministic_AI.thy +++ b/proof/invariant-abstract/X64/ArchDeterministic_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDeterministic_AI -imports "../Deterministic_AI" +imports Deterministic_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchDetype_AI.thy b/proof/invariant-abstract/X64/ArchDetype_AI.thy index 0e8778818..ba878dce4 100644 --- a/proof/invariant-abstract/X64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetype_AI.thy @@ -5,7 +5,7 @@ *) theory ArchDetype_AI -imports "../Detype_AI" +imports Detype_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy index 0ae809133..c806a6fa4 100644 --- a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy @@ -5,7 +5,7 @@ *) theory ArchEmptyFail_AI -imports "../EmptyFail_AI" +imports EmptyFail_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchFinalise_AI.thy b/proof/invariant-abstract/X64/ArchFinalise_AI.thy index 681314821..d240b7f36 100644 --- a/proof/invariant-abstract/X64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/X64/ArchFinalise_AI.thy @@ -5,7 +5,7 @@ *) theory ArchFinalise_AI -imports "../Finalise_AI" +imports Finalise_AI begin context Arch begin diff --git a/proof/invariant-abstract/X64/ArchInterruptAcc_AI.thy b/proof/invariant-abstract/X64/ArchInterruptAcc_AI.thy index 2dfc81b8c..3c11e18bb 100644 --- a/proof/invariant-abstract/X64/ArchInterruptAcc_AI.thy +++ b/proof/invariant-abstract/X64/ArchInterruptAcc_AI.thy @@ -9,7 +9,7 @@ *) theory ArchInterruptAcc_AI -imports "../InterruptAcc_AI" +imports InterruptAcc_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy index 822fdf283..adf3ecb28 100644 --- a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInterrupt_AI -imports "../Interrupt_AI" +imports Interrupt_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy index 6d0efe5e7..80ea0a2fe 100644 --- a/proof/invariant-abstract/X64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/X64/ArchInvariants_AI.thy @@ -5,7 +5,7 @@ *) theory ArchInvariants_AI -imports "../InvariantsPre_AI" "Lib.Apply_Trace_Cmd" +imports InvariantsPre_AI "Lib.Apply_Trace_Cmd" begin section "Move this up" diff --git a/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy b/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy index 3c39a1c6e..8c0562b79 100644 --- a/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpcCancel_AI -imports "../IpcCancel_AI" +imports IpcCancel_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchIpc_AI.thy b/proof/invariant-abstract/X64/ArchIpc_AI.thy index bec42b132..91acb93e8 100644 --- a/proof/invariant-abstract/X64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/X64/ArchIpc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchIpc_AI -imports "../Ipc_AI" +imports Ipc_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchKHeap_AI.thy b/proof/invariant-abstract/X64/ArchKHeap_AI.thy index 7af0bc05c..c6129095a 100644 --- a/proof/invariant-abstract/X64/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/X64/ArchKHeap_AI.thy @@ -5,7 +5,7 @@ *) theory ArchKHeap_AI -imports "../KHeapPre_AI" +imports KHeapPre_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy index 89b00498f..e0de734f5 100644 --- a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy @@ -9,9 +9,9 @@ theory ArchKernelInit_AI imports - "../ADT_AI" - "../Tcb_AI" - "../Arch_AI" + ADT_AI + Tcb_AI + Arch_AI begin context Arch begin global_naming X64 (*FIXME: arch_split*) diff --git a/proof/invariant-abstract/X64/ArchRetype_AI.thy b/proof/invariant-abstract/X64/ArchRetype_AI.thy index 575bda8c4..32b0b527c 100644 --- a/proof/invariant-abstract/X64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchRetype_AI.thy @@ -9,7 +9,7 @@ *) theory ArchRetype_AI -imports "../Retype_AI" +imports Retype_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchSchedule_AI.thy b/proof/invariant-abstract/X64/ArchSchedule_AI.thy index 534ebe6ae..bba21f234 100644 --- a/proof/invariant-abstract/X64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/X64/ArchSchedule_AI.thy @@ -5,7 +5,7 @@ *) theory ArchSchedule_AI -imports "../Schedule_AI" +imports Schedule_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchSyscall_AI.thy b/proof/invariant-abstract/X64/ArchSyscall_AI.thy index af99a0b6d..6e34aac47 100644 --- a/proof/invariant-abstract/X64/ArchSyscall_AI.thy +++ b/proof/invariant-abstract/X64/ArchSyscall_AI.thy @@ -10,7 +10,7 @@ Refinement for handleEvent and syscalls theory ArchSyscall_AI imports - "../Syscall_AI" + Syscall_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy b/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy index e032e83d3..eaef217f1 100644 --- a/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy +++ b/proof/invariant-abstract/X64/ArchTcbAcc_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcbAcc_AI -imports "../TcbAcc_AI" +imports TcbAcc_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchTcb_AI.thy b/proof/invariant-abstract/X64/ArchTcb_AI.thy index 0795e7229..012b33a32 100644 --- a/proof/invariant-abstract/X64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/X64/ArchTcb_AI.thy @@ -5,7 +5,7 @@ *) theory ArchTcb_AI -imports "../Tcb_AI" +imports Tcb_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchUntyped_AI.thy b/proof/invariant-abstract/X64/ArchUntyped_AI.thy index 219913d0a..c6f0edb8c 100644 --- a/proof/invariant-abstract/X64/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/X64/ArchUntyped_AI.thy @@ -5,7 +5,7 @@ *) theory ArchUntyped_AI -imports "../Untyped_AI" +imports Untyped_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy index 45dc3cb45..ffc6bdb71 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy @@ -5,7 +5,7 @@ *) theory ArchVSpaceEntries_AI -imports "../VSpaceEntries_AI" +imports VSpaceEntries_AI begin context Arch begin global_naming X64 (*FIXME: arch_split*) diff --git a/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy index 4f1038ff6..317445358 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy @@ -5,8 +5,9 @@ *) theory ArchVSpaceLookup_AI -imports "../SubMonad_AI" - "Lib.Crunch_Instances_NonDet" +imports + SubMonad_AI + "Lib.Crunch_Instances_NonDet" begin definition diff --git a/proof/invariant-abstract/X64/ArchVSpace_AI.thy b/proof/invariant-abstract/X64/ArchVSpace_AI.thy index 0cd3158a1..616b937cf 100644 --- a/proof/invariant-abstract/X64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpace_AI.thy @@ -9,7 +9,7 @@ X64-specific VSpace invariants *) theory ArchVSpace_AI -imports "../VSpacePre_AI" +imports VSpacePre_AI begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/Machine_AI.thy b/proof/invariant-abstract/X64/Machine_AI.thy index 6de1ba049..d38b93bca 100644 --- a/proof/invariant-abstract/X64/Machine_AI.thy +++ b/proof/invariant-abstract/X64/Machine_AI.thy @@ -9,7 +9,7 @@ Properties of machine operations. *) theory Machine_AI -imports "../Bits_AI" +imports Bits_AI begin diff --git a/proof/refine/ARM/ArchMove_R.thy b/proof/refine/ARM/ArchMove_R.thy index 065ca8aa5..9eaaefdd7 100644 --- a/proof/refine/ARM/ArchMove_R.thy +++ b/proof/refine/ARM/ArchMove_R.thy @@ -8,8 +8,7 @@ theory ArchMove_R imports - "../Move_R" - + Move_R begin (* Use one of these forms everywhere, rather than choosing at random. *) diff --git a/proof/refine/ARM_HYP/ArchMove_R.thy b/proof/refine/ARM_HYP/ArchMove_R.thy index d01bc60c9..af4b5f8af 100644 --- a/proof/refine/ARM_HYP/ArchMove_R.thy +++ b/proof/refine/ARM_HYP/ArchMove_R.thy @@ -8,8 +8,7 @@ theory ArchMove_R imports - "../Move_R" - + Move_R begin (* Use one of these forms everywhere, rather than choosing at random. *) diff --git a/proof/refine/RISCV64/ArchMove_R.thy b/proof/refine/RISCV64/ArchMove_R.thy index e3ad74374..c262c309f 100644 --- a/proof/refine/RISCV64/ArchMove_R.thy +++ b/proof/refine/RISCV64/ArchMove_R.thy @@ -8,8 +8,7 @@ theory ArchMove_R imports - "../Move_R" - + Move_R begin (* Use one of these forms everywhere, rather than choosing at random. *) diff --git a/proof/refine/X64/ArchMove_R.thy b/proof/refine/X64/ArchMove_R.thy index 2bd67bc15..eebeffd54 100644 --- a/proof/refine/X64/ArchMove_R.thy +++ b/proof/refine/X64/ArchMove_R.thy @@ -8,8 +8,7 @@ theory ArchMove_R imports - "../Move_R" - + Move_R begin (* Use one of these forms everywhere, rather than choosing at random. *) diff --git a/spec/abstract/ARM/ArchDecode_A.thy b/spec/abstract/ARM/ArchDecode_A.thy index 2a4ce85e6..1dbc7bfc0 100644 --- a/spec/abstract/ARM/ArchDecode_A.thy +++ b/spec/abstract/ARM/ArchDecode_A.thy @@ -12,8 +12,8 @@ chapter "Decoding Architecture-specific System Calls" theory ArchDecode_A imports - "../Interrupt_A" - "../InvocationLabels_A" + Interrupt_A + InvocationLabels_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchFault_A.thy b/spec/abstract/ARM/ArchFault_A.thy index 06a493243..1235e8985 100644 --- a/spec/abstract/ARM/ArchFault_A.thy +++ b/spec/abstract/ARM/ArchFault_A.thy @@ -11,7 +11,7 @@ Functions for fault handling. chapter \arch fault related functions\ theory ArchFault_A -imports "../Structures_A" "../Tcb_A" +imports Structures_A Tcb_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchInterrupt_A.thy b/spec/abstract/ARM/ArchInterrupt_A.thy index f384414f3..932acd031 100644 --- a/spec/abstract/ARM/ArchInterrupt_A.thy +++ b/spec/abstract/ARM/ArchInterrupt_A.thy @@ -11,7 +11,7 @@ Formalisation of interrupt handling. chapter "Arch-specific Interrupts" theory ArchInterrupt_A -imports "../Ipc_A" +imports Ipc_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchInvocation_A.thy b/spec/abstract/ARM/ArchInvocation_A.thy index 776954079..61d3374e0 100644 --- a/spec/abstract/ARM/ArchInvocation_A.thy +++ b/spec/abstract/ARM/ArchInvocation_A.thy @@ -11,7 +11,7 @@ Arch specific object invocations chapter "ARM Object Invocations" theory ArchInvocation_A -imports "../Structures_A" +imports Structures_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchIpcCancel_A.thy b/spec/abstract/ARM/ArchIpcCancel_A.thy index d82c0e1e4..0e7742b6c 100644 --- a/spec/abstract/ARM/ArchIpcCancel_A.thy +++ b/spec/abstract/ARM/ArchIpcCancel_A.thy @@ -10,9 +10,8 @@ Arch Functions for cancelling IPC. chapter \Arch IPC Cancelling\ - theory ArchIpcCancel_A -imports "../CSpaceAcc_A" +imports CSpaceAcc_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchTcb_A.thy b/spec/abstract/ARM/ArchTcb_A.thy index ff321685d..fa412bbe2 100644 --- a/spec/abstract/ARM/ArchTcb_A.thy +++ b/spec/abstract/ARM/ArchTcb_A.thy @@ -11,7 +11,7 @@ Arch-specific functions for the abstract model of CSpace. chapter "Architecture-specific TCB functions" theory ArchTcb_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchVSpaceAcc_A.thy b/spec/abstract/ARM/ArchVSpaceAcc_A.thy index d724190e9..e9bd3da4a 100644 --- a/spec/abstract/ARM/ArchVSpaceAcc_A.thy +++ b/spec/abstract/ARM/ArchVSpaceAcc_A.thy @@ -11,7 +11,7 @@ Accessor functions for architecture specific parts of the specification. chapter "Accessing the ARM VSpace" theory ArchVSpaceAcc_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/ArchVSpace_A.thy b/spec/abstract/ARM/ArchVSpace_A.thy index 3835a099a..83fe9eb21 100644 --- a/spec/abstract/ARM/ArchVSpace_A.thy +++ b/spec/abstract/ARM/ArchVSpace_A.thy @@ -11,7 +11,7 @@ Higher level functions for manipulating virtual address spaces chapter "ARM VSpace Functions" theory ArchVSpace_A -imports "../Retype_A" +imports Retype_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/Arch_A.thy b/spec/abstract/ARM/Arch_A.thy index 8bba04aae..17c2f5913 100644 --- a/spec/abstract/ARM/Arch_A.thy +++ b/spec/abstract/ARM/Arch_A.thy @@ -11,7 +11,7 @@ Entry point for architecture dependent definitions. chapter "Toplevel ARM Definitions" theory Arch_A -imports "../TcbAcc_A" +imports TcbAcc_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy index 5bb25a5c9..40db86cf5 100644 --- a/spec/abstract/ARM/Arch_Structs_A.thy +++ b/spec/abstract/ARM/Arch_Structs_A.thy @@ -13,8 +13,8 @@ chapter "ARM-Specific Data Types" theory Arch_Structs_A imports "ExecSpec.Arch_Structs_B" - "../ExceptionTypes_A" - "../VMRights_A" + ExceptionTypes_A + VMRights_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/Hypervisor_A.thy b/spec/abstract/ARM/Hypervisor_A.thy index efca1f236..d94a120e3 100644 --- a/spec/abstract/ARM/Hypervisor_A.thy +++ b/spec/abstract/ARM/Hypervisor_A.thy @@ -7,7 +7,7 @@ chapter "Handle Hyperviser Fault Event" theory Hypervisor_A -imports "../Exceptions_A" +imports Exceptions_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM/Init_A.thy b/spec/abstract/ARM/Init_A.thy index 7b4235cf7..9229b349a 100644 --- a/spec/abstract/ARM/Init_A.thy +++ b/spec/abstract/ARM/Init_A.thy @@ -11,7 +11,7 @@ Dummy initial kernel state. Real kernel boot up is more complex. chapter "An Initial Kernel State" theory Init_A -imports "../Retype_A" +imports Retype_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchDecode_A.thy b/spec/abstract/ARM_HYP/ArchDecode_A.thy index 4baa14a66..a69562a3e 100644 --- a/spec/abstract/ARM_HYP/ArchDecode_A.thy +++ b/spec/abstract/ARM_HYP/ArchDecode_A.thy @@ -12,7 +12,7 @@ chapter "Decoding Architecture-specific System Calls" theory ArchDecode_A imports - "../Interrupt_A" + Interrupt_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchFault_A.thy b/spec/abstract/ARM_HYP/ArchFault_A.thy index 0d48b3940..a70bd62ac 100644 --- a/spec/abstract/ARM_HYP/ArchFault_A.thy +++ b/spec/abstract/ARM_HYP/ArchFault_A.thy @@ -11,7 +11,7 @@ Functions for fault handling. chapter \arch fault related functions\ theory ArchFault_A -imports "../Structures_A" "../Tcb_A" +imports Structures_A Tcb_A begin context Arch begin global_naming ARM_HYP_A diff --git a/spec/abstract/ARM_HYP/ArchInterrupt_A.thy b/spec/abstract/ARM_HYP/ArchInterrupt_A.thy index 399d1b717..49227c818 100644 --- a/spec/abstract/ARM_HYP/ArchInterrupt_A.thy +++ b/spec/abstract/ARM_HYP/ArchInterrupt_A.thy @@ -11,7 +11,7 @@ Formalisation of interrupt handling. chapter "Arch-specific Interrupts" theory ArchInterrupt_A -imports "../Ipc_A" +imports Ipc_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchInvocation_A.thy b/spec/abstract/ARM_HYP/ArchInvocation_A.thy index a1435c604..459df77fb 100644 --- a/spec/abstract/ARM_HYP/ArchInvocation_A.thy +++ b/spec/abstract/ARM_HYP/ArchInvocation_A.thy @@ -11,7 +11,7 @@ Arch specific object invocations chapter "ARM Object Invocations" theory ArchInvocation_A -imports "../Structures_A" +imports Structures_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchIpcCancel_A.thy b/spec/abstract/ARM_HYP/ArchIpcCancel_A.thy index d82c0e1e4..0e7742b6c 100644 --- a/spec/abstract/ARM_HYP/ArchIpcCancel_A.thy +++ b/spec/abstract/ARM_HYP/ArchIpcCancel_A.thy @@ -10,9 +10,8 @@ Arch Functions for cancelling IPC. chapter \Arch IPC Cancelling\ - theory ArchIpcCancel_A -imports "../CSpaceAcc_A" +imports CSpaceAcc_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchTcb_A.thy b/spec/abstract/ARM_HYP/ArchTcb_A.thy index ac22e3d47..db887ae4c 100644 --- a/spec/abstract/ARM_HYP/ArchTcb_A.thy +++ b/spec/abstract/ARM_HYP/ArchTcb_A.thy @@ -11,7 +11,7 @@ Arch-specific functions for the abstract model of CSpace. chapter "Architecture-specific TCB functions" theory ArchTcb_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy b/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy index 8d056b44f..a54192042 100644 --- a/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy +++ b/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy @@ -11,7 +11,7 @@ Accessor functions for architecture specific parts of the specification. chapter "Accessing the ARM VSpace" theory ArchVSpaceAcc_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/ArchVSpace_A.thy b/spec/abstract/ARM_HYP/ArchVSpace_A.thy index 851e924ca..05ce37e00 100644 --- a/spec/abstract/ARM_HYP/ArchVSpace_A.thy +++ b/spec/abstract/ARM_HYP/ArchVSpace_A.thy @@ -12,8 +12,8 @@ chapter "ARM VSpace Functions" theory ArchVSpace_A imports - "../Retype_A" - "ArchTcb_A" + Retype_A + ArchTcb_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/Arch_A.thy b/spec/abstract/ARM_HYP/Arch_A.thy index dd25b2e39..f6af7d030 100644 --- a/spec/abstract/ARM_HYP/Arch_A.thy +++ b/spec/abstract/ARM_HYP/Arch_A.thy @@ -11,10 +11,9 @@ Entry point for architecture dependent definitions. chapter "Toplevel ARM Definitions" theory Arch_A -imports "../TcbAcc_A" "VCPU_A" +imports TcbAcc_A VCPU_A begin - context Arch begin global_naming ARM_A definition "page_bits \ pageBits" diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy index d5c6d1da4..2e719d615 100644 --- a/spec/abstract/ARM_HYP/Arch_Structs_A.thy +++ b/spec/abstract/ARM_HYP/Arch_Structs_A.thy @@ -13,8 +13,8 @@ chapter "ARM-Specific Data Types" theory Arch_Structs_A imports "ExecSpec.Arch_Structs_B" - "../ExceptionTypes_A" - "../VMRights_A" + ExceptionTypes_A + VMRights_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/Hypervisor_A.thy b/spec/abstract/ARM_HYP/Hypervisor_A.thy index c6194fd4e..6b811910a 100644 --- a/spec/abstract/ARM_HYP/Hypervisor_A.thy +++ b/spec/abstract/ARM_HYP/Hypervisor_A.thy @@ -7,7 +7,7 @@ chapter "Handle Hypervisor Fault Event" theory Hypervisor_A -imports "../Ipc_A" +imports Ipc_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/Init_A.thy b/spec/abstract/ARM_HYP/Init_A.thy index 8e37b2e46..a737025ba 100644 --- a/spec/abstract/ARM_HYP/Init_A.thy +++ b/spec/abstract/ARM_HYP/Init_A.thy @@ -11,7 +11,7 @@ Dummy initial kernel state. Real kernel boot up is more complex. chapter "An Initial Kernel State" theory Init_A -imports "../Retype_A" +imports Retype_A begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/VCPU_A.thy b/spec/abstract/ARM_HYP/VCPU_A.thy index 060d6551f..fedcb4912 100644 --- a/spec/abstract/ARM_HYP/VCPU_A.thy +++ b/spec/abstract/ARM_HYP/VCPU_A.thy @@ -12,9 +12,9 @@ chapter \VCPU\ theory VCPU_A imports - "../Structures_A" - "../TcbAcc_A" - "../InvocationLabels_A" + Structures_A + TcbAcc_A + InvocationLabels_A begin text \ diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy index e0586708b..b1aa4c9eb 100644 --- a/spec/abstract/CSpace_A.thy +++ b/spec/abstract/CSpace_A.thy @@ -12,9 +12,9 @@ chapter "CSpace" theory CSpace_A imports - "./$L4V_ARCH/ArchVSpace_A" + ArchVSpace_A IpcCancel_A - "./$L4V_ARCH/ArchCSpace_A" + ArchCSpace_A "Lib.NonDetMonadLemmas" "HOL-Library.Prefix_Order" begin diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index a23e89d17..5f9886e0f 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -13,7 +13,7 @@ chapter "Decoding System Calls" theory Decode_A imports Interrupt_A - "./$L4V_ARCH/ArchDecode_A" + ArchDecode_A "ExecSpec.InvocationLabels_H" begin diff --git a/spec/abstract/Interrupt_A.thy b/spec/abstract/Interrupt_A.thy index a80b7155a..91646734a 100644 --- a/spec/abstract/Interrupt_A.thy +++ b/spec/abstract/Interrupt_A.thy @@ -11,7 +11,7 @@ Formalisation of interrupt handling. chapter "Interrupts" theory Interrupt_A -imports "./$L4V_ARCH/ArchInterrupt_A" +imports ArchInterrupt_A begin context begin interpretation Arch . diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index 407c4e2f9..c9ee26ab1 100644 --- a/spec/abstract/Invocations_A.thy +++ b/spec/abstract/Invocations_A.thy @@ -11,7 +11,7 @@ Data types for syscall invocations chapter "Kernel Object Invocations" theory Invocations_A -imports "./$L4V_ARCH/ArchInvocation_A" +imports ArchInvocation_A begin context begin interpretation Arch . diff --git a/spec/abstract/IpcCancel_A.thy b/spec/abstract/IpcCancel_A.thy index 35ca661a5..f7ec1b6dc 100644 --- a/spec/abstract/IpcCancel_A.thy +++ b/spec/abstract/IpcCancel_A.thy @@ -10,9 +10,8 @@ Functions for cancelling IPC. chapter "IPC Cancelling" - theory IpcCancel_A -imports "./$L4V_ARCH/ArchIpcCancel_A" +imports ArchIpcCancel_A begin context begin interpretation Arch . diff --git a/spec/abstract/Ipc_A.thy b/spec/abstract/Ipc_A.thy index 162989cac..e41d50c73 100644 --- a/spec/abstract/Ipc_A.thy +++ b/spec/abstract/Ipc_A.thy @@ -11,7 +11,7 @@ Specification of Inter-Process Communication. chapter "IPC" theory Ipc_A -imports Tcb_A "./$L4V_ARCH/ArchFault_A" +imports Tcb_A ArchFault_A begin context begin interpretation Arch . diff --git a/spec/abstract/KernelInit_A.thy b/spec/abstract/KernelInit_A.thy index 5e6af969d..0c37e283b 100644 --- a/spec/abstract/KernelInit_A.thy +++ b/spec/abstract/KernelInit_A.thy @@ -7,7 +7,7 @@ theory KernelInit_A (* FIXME: unused, out of date *) imports Tcb_A - "./$L4V_ARCH/ArchVSpace_A" + ArchVSpace_A begin section \Generic stuff\ diff --git a/spec/abstract/MiscMachine_A.thy b/spec/abstract/MiscMachine_A.thy index 451b2bd88..ce58193ad 100644 --- a/spec/abstract/MiscMachine_A.thy +++ b/spec/abstract/MiscMachine_A.thy @@ -11,7 +11,7 @@ Utilities for the machine level which are not machine-dependent. chapter "Machine Accessor Functions" theory MiscMachine_A -imports "./$L4V_ARCH/Machine_A" "ExecSpec.MachineExports" +imports Machine_A "ExecSpec.MachineExports" begin context begin interpretation Arch . diff --git a/spec/abstract/RISCV64/ArchDecode_A.thy b/spec/abstract/RISCV64/ArchDecode_A.thy index bd87bd1ea..50b9e5ee8 100644 --- a/spec/abstract/RISCV64/ArchDecode_A.thy +++ b/spec/abstract/RISCV64/ArchDecode_A.thy @@ -8,8 +8,8 @@ chapter "Decoding Architecture-specific System Calls" theory ArchDecode_A imports - "../Interrupt_A" - "../InvocationLabels_A" + Interrupt_A + InvocationLabels_A "Word_Lib.Word_Lib" "ExecSpec.InvocationLabels_H" begin diff --git a/spec/abstract/RISCV64/ArchFault_A.thy b/spec/abstract/RISCV64/ArchFault_A.thy index 0b229fef4..601f61b15 100644 --- a/spec/abstract/RISCV64/ArchFault_A.thy +++ b/spec/abstract/RISCV64/ArchFault_A.thy @@ -7,7 +7,7 @@ chapter \Architecture-specific Fault-handling Functions\ theory ArchFault_A -imports "../Structures_A" "../Tcb_A" +imports Structures_A Tcb_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/ArchInterrupt_A.thy b/spec/abstract/RISCV64/ArchInterrupt_A.thy index c7dfd2906..05c8fdb83 100644 --- a/spec/abstract/RISCV64/ArchInterrupt_A.thy +++ b/spec/abstract/RISCV64/ArchInterrupt_A.thy @@ -7,7 +7,7 @@ chapter "Arch-specific Interrupts" theory ArchInterrupt_A -imports "../Ipc_A" +imports Ipc_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/ArchInvocation_A.thy b/spec/abstract/RISCV64/ArchInvocation_A.thy index 7912613e7..d89712d68 100644 --- a/spec/abstract/RISCV64/ArchInvocation_A.thy +++ b/spec/abstract/RISCV64/ArchInvocation_A.thy @@ -7,7 +7,7 @@ chapter "RISCV64 Object Invocations" theory ArchInvocation_A -imports "../Structures_A" +imports Structures_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/ArchIpcCancel_A.thy b/spec/abstract/RISCV64/ArchIpcCancel_A.thy index 0b296f980..da53340db 100644 --- a/spec/abstract/RISCV64/ArchIpcCancel_A.thy +++ b/spec/abstract/RISCV64/ArchIpcCancel_A.thy @@ -7,7 +7,7 @@ chapter \Arch IPC Cancelling\ theory ArchIpcCancel_A -imports "../CSpaceAcc_A" +imports CSpaceAcc_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/ArchTcb_A.thy b/spec/abstract/RISCV64/ArchTcb_A.thy index 733aaac6b..b96b5e753 100644 --- a/spec/abstract/RISCV64/ArchTcb_A.thy +++ b/spec/abstract/RISCV64/ArchTcb_A.thy @@ -7,7 +7,7 @@ chapter "Architecture-specific TCB functions" theory ArchTcb_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/ArchVSpaceAcc_A.thy b/spec/abstract/RISCV64/ArchVSpaceAcc_A.thy index f1b976a14..5e6044776 100644 --- a/spec/abstract/RISCV64/ArchVSpaceAcc_A.thy +++ b/spec/abstract/RISCV64/ArchVSpaceAcc_A.thy @@ -7,7 +7,7 @@ chapter "Accessing the RISCV64 VSpace" theory ArchVSpaceAcc_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/ArchVSpace_A.thy b/spec/abstract/RISCV64/ArchVSpace_A.thy index 986bae327..b7b1aed38 100644 --- a/spec/abstract/RISCV64/ArchVSpace_A.thy +++ b/spec/abstract/RISCV64/ArchVSpace_A.thy @@ -7,7 +7,7 @@ chapter "RISCV64 VSpace Functions" theory ArchVSpace_A -imports "../Retype_A" +imports Retype_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/Arch_A.thy b/spec/abstract/RISCV64/Arch_A.thy index 52bdd6bf7..ee64de9c0 100644 --- a/spec/abstract/RISCV64/Arch_A.thy +++ b/spec/abstract/RISCV64/Arch_A.thy @@ -7,7 +7,7 @@ chapter "Toplevel RISCV64 Definitions" theory Arch_A -imports "../TcbAcc_A" +imports TcbAcc_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/Arch_Structs_A.thy b/spec/abstract/RISCV64/Arch_Structs_A.thy index 06a810669..92468fe72 100644 --- a/spec/abstract/RISCV64/Arch_Structs_A.thy +++ b/spec/abstract/RISCV64/Arch_Structs_A.thy @@ -9,8 +9,8 @@ chapter "RISCV64-Specific Data Types" theory Arch_Structs_A imports "ExecSpec.Arch_Structs_B" - "../ExceptionTypes_A" - "../VMRights_A" + ExceptionTypes_A + VMRights_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/Hypervisor_A.thy b/spec/abstract/RISCV64/Hypervisor_A.thy index f1fa1577b..6d14378b2 100644 --- a/spec/abstract/RISCV64/Hypervisor_A.thy +++ b/spec/abstract/RISCV64/Hypervisor_A.thy @@ -7,7 +7,7 @@ chapter "Handle Hypervisor Fault Events" theory Hypervisor_A -imports "../Exceptions_A" +imports Exceptions_A begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/RISCV64/Init_A.thy b/spec/abstract/RISCV64/Init_A.thy index d6db46bf7..8ee8cc59b 100644 --- a/spec/abstract/RISCV64/Init_A.thy +++ b/spec/abstract/RISCV64/Init_A.thy @@ -7,8 +7,9 @@ chapter "An Initial Kernel State" theory Init_A -imports "../Retype_A" -"Lib.SplitRule" +imports + Retype_A + "Lib.SplitRule" begin context Arch begin global_naming RISCV64_A diff --git a/spec/abstract/Retype_A.thy b/spec/abstract/Retype_A.thy index c10882722..2d5ed15f5 100644 --- a/spec/abstract/Retype_A.thy +++ b/spec/abstract/Retype_A.thy @@ -13,9 +13,9 @@ chapter "Retyping and Untyped Invocations" theory Retype_A imports CSpaceAcc_A - "./$L4V_ARCH/ArchVSpaceAcc_A" + ArchVSpaceAcc_A Invocations_A - "./$L4V_ARCH/ArchRetype_A" + ArchRetype_A begin context begin interpretation Arch . diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy index 73826df02..018c088ca 100644 --- a/spec/abstract/Schedule_A.thy +++ b/spec/abstract/Schedule_A.thy @@ -11,7 +11,7 @@ Non-deterministic scheduler functionality. chapter "Scheduler" theory Schedule_A -imports "./$L4V_ARCH/Arch_A" +imports Arch_A begin context begin interpretation Arch . diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index 8448f85b3..273cf00c5 100644 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -13,9 +13,8 @@ chapter "Basic Data Structures" theory Structures_A imports - "./$L4V_ARCH/Arch_Structs_A" + Arch_Structs_A "ExecSpec.MachineExports" - begin context begin interpretation Arch . diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy index 10128e940..f4ea1d656 100644 --- a/spec/abstract/Syscall_A.thy +++ b/spec/abstract/Syscall_A.thy @@ -14,8 +14,8 @@ theory Syscall_A imports "ExecSpec.Event_H" Decode_A - "./$L4V_ARCH/Init_A" - "./$L4V_ARCH/Hypervisor_A" + Init_A + Hypervisor_A begin context begin interpretation Arch . diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index 0cf069306..2d62bf9ed 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -11,7 +11,7 @@ The TCB and thread related specifications. chapter "Threads and TCBs" theory Tcb_A -imports TcbAcc_A Schedule_A "$L4V_ARCH/ArchTcb_A" +imports TcbAcc_A Schedule_A ArchTcb_A begin context begin interpretation Arch . diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy index adb28b774..36acca4d0 100644 --- a/spec/abstract/X64/ArchDecode_A.thy +++ b/spec/abstract/X64/ArchDecode_A.thy @@ -12,8 +12,8 @@ chapter "Decoding Architecture-specific System Calls" theory ArchDecode_A imports - "../Interrupt_A" - "../InvocationLabels_A" + Interrupt_A + InvocationLabels_A "Word_Lib.Word_Lib" "ExecSpec.InvocationLabels_H" begin diff --git a/spec/abstract/X64/ArchFault_A.thy b/spec/abstract/X64/ArchFault_A.thy index e940ba2d1..e42acf552 100644 --- a/spec/abstract/X64/ArchFault_A.thy +++ b/spec/abstract/X64/ArchFault_A.thy @@ -11,7 +11,7 @@ Functions for fault handling. chapter \arch fault related functions\ theory ArchFault_A -imports "../Structures_A" "../Tcb_A" +imports Structures_A Tcb_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/ArchInterrupt_A.thy b/spec/abstract/X64/ArchInterrupt_A.thy index 14e471f40..0330bdfcb 100644 --- a/spec/abstract/X64/ArchInterrupt_A.thy +++ b/spec/abstract/X64/ArchInterrupt_A.thy @@ -11,7 +11,7 @@ Formalisation of interrupt handling. chapter "Arch-specific Interrupts" theory ArchInterrupt_A -imports "../Ipc_A" +imports Ipc_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/ArchInvocation_A.thy b/spec/abstract/X64/ArchInvocation_A.thy index fa23226f4..567cf9c6a 100644 --- a/spec/abstract/X64/ArchInvocation_A.thy +++ b/spec/abstract/X64/ArchInvocation_A.thy @@ -11,7 +11,7 @@ Arch specific object invocations chapter "x64 Object Invocations" theory ArchInvocation_A -imports "../Structures_A" +imports Structures_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/ArchIpcCancel_A.thy b/spec/abstract/X64/ArchIpcCancel_A.thy index a865eda3d..914fe612e 100644 --- a/spec/abstract/X64/ArchIpcCancel_A.thy +++ b/spec/abstract/X64/ArchIpcCancel_A.thy @@ -10,9 +10,8 @@ Arch Functions for cancelling IPC. chapter \Arch IPC Cancelling\ - theory ArchIpcCancel_A -imports "../CSpaceAcc_A" +imports CSpaceAcc_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/ArchTcb_A.thy b/spec/abstract/X64/ArchTcb_A.thy index def224dc7..b6c44d2cd 100644 --- a/spec/abstract/X64/ArchTcb_A.thy +++ b/spec/abstract/X64/ArchTcb_A.thy @@ -11,7 +11,7 @@ Arch-specific functions for the abstract model of CSpace. chapter "Architecture-specific TCB functions" theory ArchTcb_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/ArchVSpaceAcc_A.thy b/spec/abstract/X64/ArchVSpaceAcc_A.thy index 554885da6..ed78d47cc 100644 --- a/spec/abstract/X64/ArchVSpaceAcc_A.thy +++ b/spec/abstract/X64/ArchVSpaceAcc_A.thy @@ -11,7 +11,7 @@ Accessor functions for architecture specific parts of the specification. chapter "Accessing the x64 VSpace" theory ArchVSpaceAcc_A -imports "../KHeap_A" +imports KHeap_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/ArchVSpace_A.thy b/spec/abstract/X64/ArchVSpace_A.thy index 3ee0733b7..277e94487 100644 --- a/spec/abstract/X64/ArchVSpace_A.thy +++ b/spec/abstract/X64/ArchVSpace_A.thy @@ -11,7 +11,7 @@ Higher level functions for manipulating virtual address spaces chapter "x64 VSpace Functions" theory ArchVSpace_A -imports "../Retype_A" +imports Retype_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy index a80ca8d09..a52370eba 100644 --- a/spec/abstract/X64/Arch_A.thy +++ b/spec/abstract/X64/Arch_A.thy @@ -11,7 +11,7 @@ Entry point for architecture dependent definitions. chapter "Toplevel x64 Definitions" theory Arch_A -imports "../TcbAcc_A" +imports TcbAcc_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy index afccd0bb1..235fbc93d 100644 --- a/spec/abstract/X64/Arch_Structs_A.thy +++ b/spec/abstract/X64/Arch_Structs_A.thy @@ -9,8 +9,8 @@ chapter "x64-Specific Data Types" theory Arch_Structs_A imports "ExecSpec.Arch_Structs_B" - "../ExceptionTypes_A" - "../VMRights_A" + ExceptionTypes_A + VMRights_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/Hypervisor_A.thy b/spec/abstract/X64/Hypervisor_A.thy index 4c5977bef..330679f8b 100644 --- a/spec/abstract/X64/Hypervisor_A.thy +++ b/spec/abstract/X64/Hypervisor_A.thy @@ -7,7 +7,7 @@ chapter "Handle Hyperviser Fault Event" theory Hypervisor_A -imports "../Exceptions_A" +imports Exceptions_A begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/Init_A.thy b/spec/abstract/X64/Init_A.thy index d2c90afac..1d78c1a7d 100644 --- a/spec/abstract/X64/Init_A.thy +++ b/spec/abstract/X64/Init_A.thy @@ -11,7 +11,7 @@ Dummy initial kernel state. Real kernel boot up is more complex. chapter "An Initial Kernel State" theory Init_A -imports "../Retype_A" +imports Retype_A begin context Arch begin global_naming X64_A diff --git a/spec/cspec/KernelInc_C.thy b/spec/cspec/KernelInc_C.thy index c32b39613..bf66d4556 100644 --- a/spec/cspec/KernelInc_C.thy +++ b/spec/cspec/KernelInc_C.thy @@ -7,10 +7,10 @@ theory KernelInc_C imports "Substitute" - "c/build/$L4V_ARCH/generated/arch/object/structures_defs" - "c/build/$L4V_ARCH/generated/arch/object/structures_proofs" - "c/build/$L4V_ARCH/generated/sel4/shared_types_defs" - "c/build/$L4V_ARCH/generated/sel4/shared_types_proofs" + "structures_defs" + "structures_proofs" + "shared_types_defs" + "shared_types_proofs" begin end diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index fe4c99c86..103ef0a17 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/spec/design/m-skel/ARM/MachineTypes.thy @@ -10,7 +10,7 @@ theory MachineTypes imports "Word_Lib.WordSetup" "Lib.OptionMonadND" - "../Setup_Locale" + Setup_Locale Platform begin diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy index 90b25a805..8418a9b7d 100644 --- a/spec/design/m-skel/ARM_HYP/MachineTypes.thy +++ b/spec/design/m-skel/ARM_HYP/MachineTypes.thy @@ -10,7 +10,7 @@ theory MachineTypes imports "Word_Lib.WordSetup" "Lib.OptionMonadND" - "../Setup_Locale" + Setup_Locale Platform begin context Arch begin global_naming ARM_HYP diff --git a/spec/design/skel/ARM/ArchFaultHandler_H.thy b/spec/design/skel/ARM/ArchFaultHandler_H.thy index f07085981..e0729561d 100644 --- a/spec/design/skel/ARM/ArchFaultHandler_H.thy +++ b/spec/design/skel/ARM/ArchFaultHandler_H.thy @@ -7,7 +7,7 @@ chapter "Fault Handlers" theory ArchFaultHandler_H -imports "../TCB_H" "../Structures_H" +imports TCB_H Structures_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchFault_H.thy b/spec/design/skel/ARM/ArchFault_H.thy index 6ad63fb14..0348207fa 100644 --- a/spec/design/skel/ARM/ArchFault_H.thy +++ b/spec/design/skel/ARM/ArchFault_H.thy @@ -9,7 +9,7 @@ *) theory ArchFault_H -imports "../Types_H" +imports Types_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchHypervisor_H.thy b/spec/design/skel/ARM/ArchHypervisor_H.thy index 5bc9c8b0f..a0e218c7c 100644 --- a/spec/design/skel/ARM/ArchHypervisor_H.thy +++ b/spec/design/skel/ARM/ArchHypervisor_H.thy @@ -10,9 +10,9 @@ theory ArchHypervisor_H imports - "../CNode_H" - "../KI_Decls_H" - "../InterruptDecls_H" + CNode_H + KI_Decls_H + InterruptDecls_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchIntermediate_H.thy b/spec/design/skel/ARM/ArchIntermediate_H.thy index 0b3953a57..2cbf1f9cc 100644 --- a/spec/design/skel/ARM/ArchIntermediate_H.thy +++ b/spec/design/skel/ARM/ArchIntermediate_H.thy @@ -7,7 +7,7 @@ chapter "Intermediate" theory ArchIntermediate_H -imports "../Intermediate_H" +imports Intermediate_H begin context Arch begin diff --git a/spec/design/skel/ARM/ArchInterruptDecls_H.thy b/spec/design/skel/ARM/ArchInterruptDecls_H.thy index 64425c6ff..e620da721 100644 --- a/spec/design/skel/ARM/ArchInterruptDecls_H.thy +++ b/spec/design/skel/ARM/ArchInterruptDecls_H.thy @@ -5,7 +5,7 @@ *) theory ArchInterruptDecls_H -imports "../RetypeDecls_H" "../CNode_H" +imports RetypeDecls_H CNode_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchInterrupt_H.thy b/spec/design/skel/ARM/ArchInterrupt_H.thy index f257313a1..c255cb8a7 100644 --- a/spec/design/skel/ARM/ArchInterrupt_H.thy +++ b/spec/design/skel/ARM/ArchInterrupt_H.thy @@ -6,9 +6,9 @@ theory ArchInterrupt_H imports - "../RetypeDecls_H" - "../CNode_H" - "../InterruptDecls_H" + RetypeDecls_H + CNode_H + InterruptDecls_H ArchInterruptDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/ARM/ArchInvocationLabels_H.thy b/spec/design/skel/ARM/ArchInvocationLabels_H.thy index 1a3a8f241..f09d72dc5 100644 --- a/spec/design/skel/ARM/ArchInvocationLabels_H.thy +++ b/spec/design/skel/ARM/ArchInvocationLabels_H.thy @@ -9,7 +9,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports "Word_Lib.Enumeration" - "../../machine/Setup_Locale" + Setup_Locale begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchLabelFuns_H.thy b/spec/design/skel/ARM/ArchLabelFuns_H.thy index d3806afa5..2011bda04 100644 --- a/spec/design/skel/ARM/ArchLabelFuns_H.thy +++ b/spec/design/skel/ARM/ArchLabelFuns_H.thy @@ -7,7 +7,7 @@ chapter "Architecture-specific Invocation Label Functions" theory ArchLabelFuns_H -imports "../InvocationLabels_H" +imports InvocationLabels_H begin context Arch begin global_naming ARM_H text \ diff --git a/spec/design/skel/ARM/ArchObjInsts_H.thy b/spec/design/skel/ARM/ArchObjInsts_H.thy index f4f457e17..0a7b1a8dc 100644 --- a/spec/design/skel/ARM/ArchObjInsts_H.thy +++ b/spec/design/skel/ARM/ArchObjInsts_H.thy @@ -13,8 +13,8 @@ chapter "Storable Arch Object Instances" theory ArchObjInsts_H imports ArchTypes_H - "../PSpaceStorable_H" - "../ObjectInstances_H" + PSpaceStorable_H + ObjectInstances_H begin qualify ARM_H (in Arch) diff --git a/spec/design/skel/ARM/ArchRetypeDecls_H.thy b/spec/design/skel/ARM/ArchRetypeDecls_H.thy index c306b76bd..ceef16202 100644 --- a/spec/design/skel/ARM/ArchRetypeDecls_H.thy +++ b/spec/design/skel/ARM/ArchRetypeDecls_H.thy @@ -9,10 +9,10 @@ chapter "Retyping Objects" theory ArchRetypeDecls_H imports ArchLabelFuns_H - "../FaultMonad_H" - "../EndpointDecls_H" - "../KernelInitMonad_H" - "../PSpaceFuns_H" + FaultMonad_H + EndpointDecls_H + KernelInitMonad_H + PSpaceFuns_H ArchObjInsts_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchRetype_H.thy b/spec/design/skel/ARM/ArchRetype_H.thy index b09db1046..c5516ab04 100644 --- a/spec/design/skel/ARM/ArchRetype_H.thy +++ b/spec/design/skel/ARM/ArchRetype_H.thy @@ -11,7 +11,7 @@ imports ArchRetypeDecls_H ArchVSpaceDecls_H Hardware_H - "../KI_Decls_H" + KI_Decls_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchStructures_H.thy b/spec/design/skel/ARM/ArchStructures_H.thy index 050c8c782..ced98a935 100644 --- a/spec/design/skel/ARM/ArchStructures_H.thy +++ b/spec/design/skel/ARM/ArchStructures_H.thy @@ -7,7 +7,7 @@ theory ArchStructures_H imports "Lib.Lib" - "../Types_H" + Types_H Hardware_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchTCB_H.thy b/spec/design/skel/ARM/ArchTCB_H.thy index 9282e2f34..a3fd51156 100644 --- a/spec/design/skel/ARM/ArchTCB_H.thy +++ b/spec/design/skel/ARM/ArchTCB_H.thy @@ -5,7 +5,7 @@ *) theory ArchTCB_H -imports "../TCBDecls_H" +imports TCBDecls_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchThreadDecls_H.thy b/spec/design/skel/ARM/ArchThreadDecls_H.thy index d03526040..3536521e5 100644 --- a/spec/design/skel/ARM/ArchThreadDecls_H.thy +++ b/spec/design/skel/ARM/ArchThreadDecls_H.thy @@ -12,9 +12,9 @@ chapter "Function Declarations for Threads" theory ArchThreadDecls_H imports - "../Structures_H" - "../FaultMonad_H" - "../KernelInitMonad_H" + Structures_H + FaultMonad_H + KernelInitMonad_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchThread_H.thy b/spec/design/skel/ARM/ArchThread_H.thy index 87f8dc8d5..4661bd058 100644 --- a/spec/design/skel/ARM/ArchThread_H.thy +++ b/spec/design/skel/ARM/ArchThread_H.thy @@ -9,7 +9,7 @@ chapter "Threads" theory ArchThread_H imports ArchThreadDecls_H - "../TCBDecls_H" + TCBDecls_H ArchVSpaceDecls_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchVSpaceDecls_H.thy b/spec/design/skel/ARM/ArchVSpaceDecls_H.thy index ae9cacc5e..cae8b84d6 100644 --- a/spec/design/skel/ARM/ArchVSpaceDecls_H.thy +++ b/spec/design/skel/ARM/ArchVSpaceDecls_H.thy @@ -7,7 +7,7 @@ chapter "Retyping Objects" theory ArchVSpaceDecls_H -imports ArchRetypeDecls_H "../InvocationLabels_H" +imports ArchRetypeDecls_H InvocationLabels_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchVSpace_H.thy b/spec/design/skel/ARM/ArchVSpace_H.thy index 307db8d41..8ef22eb02 100644 --- a/spec/design/skel/ARM/ArchVSpace_H.thy +++ b/spec/design/skel/ARM/ArchVSpace_H.thy @@ -10,9 +10,9 @@ theory ArchVSpace_H imports - "../CNode_H" - "../Untyped_H" - "../KI_Decls_H" + CNode_H + Untyped_H + KI_Decls_H ArchVSpaceDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/ARM/Arch_Structs_B.thy b/spec/design/skel/ARM/Arch_Structs_B.thy index 6341ffe4f..188feeedf 100644 --- a/spec/design/skel/ARM/Arch_Structs_B.thy +++ b/spec/design/skel/ARM/Arch_Structs_B.thy @@ -9,7 +9,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports Main "../../../spec/machine/Setup_Locale" +imports Main Setup_Locale begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/Hardware_H.thy b/spec/design/skel/ARM/Hardware_H.thy index 446052637..3da78daca 100644 --- a/spec/design/skel/ARM/Hardware_H.thy +++ b/spec/design/skel/ARM/Hardware_H.thy @@ -6,7 +6,7 @@ theory Hardware_H imports - "../../machine/ARM/MachineOps" + MachineOps State_H begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/RegisterSet_H.thy b/spec/design/skel/ARM/RegisterSet_H.thy index a11a9a71a..7af02c03e 100644 --- a/spec/design/skel/ARM/RegisterSet_H.thy +++ b/spec/design/skel/ARM/RegisterSet_H.thy @@ -9,7 +9,7 @@ chapter "Register Set" theory RegisterSet_H imports "Lib.HaskellLib_H" - "../../machine/ARM/MachineTypes" + MachineTypes begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/State_H.thy b/spec/design/skel/ARM/State_H.thy index e0a4097b7..ca3dd1891 100644 --- a/spec/design/skel/ARM/State_H.thy +++ b/spec/design/skel/ARM/State_H.thy @@ -14,7 +14,7 @@ theory State_H imports "Lib.HaskellLib_H" RegisterSet_H - "../../machine/ARM/MachineOps" + MachineOps begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM_HYP/ArchFaultHandler_H.thy b/spec/design/skel/ARM_HYP/ArchFaultHandler_H.thy index 6c762eaff..f7a0255de 100644 --- a/spec/design/skel/ARM_HYP/ArchFaultHandler_H.thy +++ b/spec/design/skel/ARM_HYP/ArchFaultHandler_H.thy @@ -7,7 +7,7 @@ chapter "Fault Handlers" theory ArchFaultHandler_H -imports "../TCB_H" "../Structures_H" +imports TCB_H Structures_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchFault_H.thy b/spec/design/skel/ARM_HYP/ArchFault_H.thy index a5e0f8f67..818492b1d 100644 --- a/spec/design/skel/ARM_HYP/ArchFault_H.thy +++ b/spec/design/skel/ARM_HYP/ArchFault_H.thy @@ -9,9 +9,7 @@ *) theory ArchFault_H -imports "../Types_H" -(* "../KI_Decls_H" - ArchVSpaceDecls_H *) +imports Types_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchHypervisor_H.thy b/spec/design/skel/ARM_HYP/ArchHypervisor_H.thy index 28c41d0d4..4043575bf 100644 --- a/spec/design/skel/ARM_HYP/ArchHypervisor_H.thy +++ b/spec/design/skel/ARM_HYP/ArchHypervisor_H.thy @@ -10,9 +10,9 @@ theory ArchHypervisor_H imports - "../CNode_H" - "../FaultHandlerDecls_H" - "../InterruptDecls_H" + CNode_H + FaultHandlerDecls_H + InterruptDecls_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchIntermediate_H.thy b/spec/design/skel/ARM_HYP/ArchIntermediate_H.thy index f60763ef7..9b1261671 100644 --- a/spec/design/skel/ARM_HYP/ArchIntermediate_H.thy +++ b/spec/design/skel/ARM_HYP/ArchIntermediate_H.thy @@ -7,7 +7,7 @@ chapter "Intermediate" theory ArchIntermediate_H -imports "../Intermediate_H" +imports Intermediate_H begin context Arch begin diff --git a/spec/design/skel/ARM_HYP/ArchInterruptDecls_H.thy b/spec/design/skel/ARM_HYP/ArchInterruptDecls_H.thy index ed8be2f34..8aa686f3e 100644 --- a/spec/design/skel/ARM_HYP/ArchInterruptDecls_H.thy +++ b/spec/design/skel/ARM_HYP/ArchInterruptDecls_H.thy @@ -5,7 +5,7 @@ *) theory ArchInterruptDecls_H -imports "../RetypeDecls_H" "../CNode_H" +imports RetypeDecls_H CNode_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy b/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy index 5780dbd3e..468526e5d 100644 --- a/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy +++ b/spec/design/skel/ARM_HYP/ArchInterrupt_H.thy @@ -6,9 +6,9 @@ theory ArchInterrupt_H imports - "../RetypeDecls_H" - "../CNode_H" - "../InterruptDecls_H" + RetypeDecls_H + CNode_H + InterruptDecls_H ArchInterruptDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy b/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy index 7814cfbf2..bbfce9692 100644 --- a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy +++ b/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy @@ -9,7 +9,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports "Word_Lib.Enumeration" - "../../machine/Setup_Locale" + Setup_Locale begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchLabelFuns_H.thy b/spec/design/skel/ARM_HYP/ArchLabelFuns_H.thy index 1690ecb0f..769893835 100644 --- a/spec/design/skel/ARM_HYP/ArchLabelFuns_H.thy +++ b/spec/design/skel/ARM_HYP/ArchLabelFuns_H.thy @@ -7,7 +7,7 @@ chapter "Architecture-specific Invocation Label Functions" theory ArchLabelFuns_H -imports "../InvocationLabels_H" +imports InvocationLabels_H begin context Arch begin global_naming ARM_HYP_H text \ diff --git a/spec/design/skel/ARM_HYP/ArchObjInsts_H.thy b/spec/design/skel/ARM_HYP/ArchObjInsts_H.thy index 5afb620fd..588359db4 100644 --- a/spec/design/skel/ARM_HYP/ArchObjInsts_H.thy +++ b/spec/design/skel/ARM_HYP/ArchObjInsts_H.thy @@ -13,8 +13,8 @@ chapter "Storable Arch Object Instances" theory ArchObjInsts_H imports ArchTypes_H - "../PSpaceStorable_H" - "../ObjectInstances_H" + PSpaceStorable_H + ObjectInstances_H begin qualify ARM_HYP_H (in Arch) diff --git a/spec/design/skel/ARM_HYP/ArchRetypeDecls_H.thy b/spec/design/skel/ARM_HYP/ArchRetypeDecls_H.thy index 7d9efb8e8..004b3395b 100644 --- a/spec/design/skel/ARM_HYP/ArchRetypeDecls_H.thy +++ b/spec/design/skel/ARM_HYP/ArchRetypeDecls_H.thy @@ -9,10 +9,10 @@ chapter "Retyping Objects" theory ArchRetypeDecls_H imports ArchLabelFuns_H - "../FaultMonad_H" - "../EndpointDecls_H" - "../KernelInitMonad_H" - "../PSpaceFuns_H" + FaultMonad_H + EndpointDecls_H + KernelInitMonad_H + PSpaceFuns_H ArchObjInsts_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchRetype_H.thy b/spec/design/skel/ARM_HYP/ArchRetype_H.thy index 5a334f7bf..ea516d86c 100644 --- a/spec/design/skel/ARM_HYP/ArchRetype_H.thy +++ b/spec/design/skel/ARM_HYP/ArchRetype_H.thy @@ -12,7 +12,7 @@ imports ArchVSpaceDecls_H Hardware_H VCPU_H - "../KI_Decls_H" + KI_Decls_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchStructures_H.thy b/spec/design/skel/ARM_HYP/ArchStructures_H.thy index e4717d72a..47bf8628e 100644 --- a/spec/design/skel/ARM_HYP/ArchStructures_H.thy +++ b/spec/design/skel/ARM_HYP/ArchStructures_H.thy @@ -7,7 +7,7 @@ theory ArchStructures_H imports "Lib.Lib" - "../Types_H" + Types_H Hardware_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchTCB_H.thy b/spec/design/skel/ARM_HYP/ArchTCB_H.thy index 17e25e5ac..d01651eb2 100644 --- a/spec/design/skel/ARM_HYP/ArchTCB_H.thy +++ b/spec/design/skel/ARM_HYP/ArchTCB_H.thy @@ -5,7 +5,7 @@ *) theory ArchTCB_H -imports "../TCBDecls_H" +imports TCBDecls_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchThreadDecls_H.thy b/spec/design/skel/ARM_HYP/ArchThreadDecls_H.thy index edab28ce2..fcfa48857 100644 --- a/spec/design/skel/ARM_HYP/ArchThreadDecls_H.thy +++ b/spec/design/skel/ARM_HYP/ArchThreadDecls_H.thy @@ -12,9 +12,9 @@ chapter "Function Declarations for Threads" theory ArchThreadDecls_H imports - "../Structures_H" - "../FaultMonad_H" - "../KernelInitMonad_H" + Structures_H + FaultMonad_H + KernelInitMonad_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchThread_H.thy b/spec/design/skel/ARM_HYP/ArchThread_H.thy index 38b3deeaa..514d097ee 100644 --- a/spec/design/skel/ARM_HYP/ArchThread_H.thy +++ b/spec/design/skel/ARM_HYP/ArchThread_H.thy @@ -9,7 +9,7 @@ chapter "Threads" theory ArchThread_H imports ArchThreadDecls_H - "../TCBDecls_H" + TCBDecls_H ArchVSpaceDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/ARM_HYP/ArchVSpaceDecls_H.thy b/spec/design/skel/ARM_HYP/ArchVSpaceDecls_H.thy index 371563ec3..da0372748 100644 --- a/spec/design/skel/ARM_HYP/ArchVSpaceDecls_H.thy +++ b/spec/design/skel/ARM_HYP/ArchVSpaceDecls_H.thy @@ -7,7 +7,7 @@ chapter "Retyping Objects" theory ArchVSpaceDecls_H -imports ArchRetypeDecls_H "../InvocationLabels_H" +imports ArchRetypeDecls_H InvocationLabels_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchVSpace_H.thy b/spec/design/skel/ARM_HYP/ArchVSpace_H.thy index 7777824b5..6828c5940 100644 --- a/spec/design/skel/ARM_HYP/ArchVSpace_H.thy +++ b/spec/design/skel/ARM_HYP/ArchVSpace_H.thy @@ -10,8 +10,8 @@ theory ArchVSpace_H imports - "../CNode_H" - "../KI_Decls_H" + CNode_H + KI_Decls_H ArchVSpaceDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy index c73a8b925..4b5ae6373 100644 --- a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy +++ b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy @@ -9,7 +9,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports Main "../../machine/Setup_Locale" +imports Main Setup_Locale begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/Hardware_H.thy b/spec/design/skel/ARM_HYP/Hardware_H.thy index c89f93ee8..754dedd7c 100644 --- a/spec/design/skel/ARM_HYP/Hardware_H.thy +++ b/spec/design/skel/ARM_HYP/Hardware_H.thy @@ -6,7 +6,7 @@ theory Hardware_H imports - "../../machine/ARM_HYP/MachineOps" + MachineOps State_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/RegisterSet_H.thy b/spec/design/skel/ARM_HYP/RegisterSet_H.thy index 6d440d90b..b3f2196a2 100644 --- a/spec/design/skel/ARM_HYP/RegisterSet_H.thy +++ b/spec/design/skel/ARM_HYP/RegisterSet_H.thy @@ -9,7 +9,7 @@ chapter "Register Set" theory RegisterSet_H imports "Lib.HaskellLib_H" - "../../machine/ARM_HYP/MachineTypes" + MachineTypes begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/State_H.thy b/spec/design/skel/ARM_HYP/State_H.thy index 25013a712..f968b2674 100644 --- a/spec/design/skel/ARM_HYP/State_H.thy +++ b/spec/design/skel/ARM_HYP/State_H.thy @@ -14,7 +14,7 @@ theory State_H imports "Lib.HaskellLib_H" RegisterSet_H - "../../machine/ARM_HYP/MachineOps" + MachineOps begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/VCPU_H.thy b/spec/design/skel/ARM_HYP/VCPU_H.thy index a22c433b3..05376c7f6 100644 --- a/spec/design/skel/ARM_HYP/VCPU_H.thy +++ b/spec/design/skel/ARM_HYP/VCPU_H.thy @@ -7,9 +7,11 @@ chapter "VCPU" theory VCPU_H -imports Hardware_H "../Structures_H" - "../Invocations_H" - "../TCB_H" +imports + Hardware_H + Structures_H + Invocations_H + TCB_H begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/Event_H.thy b/spec/design/skel/Event_H.thy index 8e035d928..ad777aced 100644 --- a/spec/design/skel/Event_H.thy +++ b/spec/design/skel/Event_H.thy @@ -7,7 +7,7 @@ chapter "Kernel Events" theory Event_H -imports "../machine/MachineExports" +imports MachineExports begin text \ diff --git a/spec/design/skel/FaultHandler_H.thy b/spec/design/skel/FaultHandler_H.thy index c14f94b1c..f1e584b79 100644 --- a/spec/design/skel/FaultHandler_H.thy +++ b/spec/design/skel/FaultHandler_H.thy @@ -7,8 +7,10 @@ chapter "Fault Handlers" theory FaultHandler_H -imports FaultHandlerDecls_H TCB_H - "./$L4V_ARCH/ArchFaultHandler_H" +imports + FaultHandlerDecls_H + TCB_H + ArchFaultHandler_H begin context begin interpretation Arch . diff --git a/spec/design/skel/Fault_H.thy b/spec/design/skel/Fault_H.thy index 12c3cab7e..96848f7ff 100644 --- a/spec/design/skel/Fault_H.thy +++ b/spec/design/skel/Fault_H.thy @@ -11,7 +11,7 @@ chapter "Fault Structures" theory Fault_H -imports "$L4V_ARCH/ArchFault_H" +imports ArchFault_H begin context begin interpretation Arch . diff --git a/spec/design/skel/Hypervisor_H.thy b/spec/design/skel/Hypervisor_H.thy index f991cf2c6..ee49f7da9 100644 --- a/spec/design/skel/Hypervisor_H.thy +++ b/spec/design/skel/Hypervisor_H.thy @@ -11,7 +11,7 @@ theory Hypervisor_H imports CNode_H - "./$L4V_ARCH/ArchHypervisor_H" + ArchHypervisor_H KernelInitMonad_H begin diff --git a/spec/design/skel/Interrupt_H.thy b/spec/design/skel/Interrupt_H.thy index 973055963..ba26a329d 100644 --- a/spec/design/skel/Interrupt_H.thy +++ b/spec/design/skel/Interrupt_H.thy @@ -7,7 +7,7 @@ theory Interrupt_H imports RetypeDecls_H - "./$L4V_ARCH/ArchInterrupt_H" + ArchInterrupt_H Notification_H CNode_H KI_Decls_H diff --git a/spec/design/skel/InvocationLabels_H.thy b/spec/design/skel/InvocationLabels_H.thy index de671ecd9..faa65f824 100644 --- a/spec/design/skel/InvocationLabels_H.thy +++ b/spec/design/skel/InvocationLabels_H.thy @@ -7,7 +7,7 @@ chapter "Kernel Invocation Labels" theory InvocationLabels_H -imports "$L4V_ARCH/ArchInvocationLabels_H" +imports ArchInvocationLabels_H begin context begin interpretation Arch . diff --git a/spec/design/skel/Invocations_H.thy b/spec/design/skel/Invocations_H.thy index 1d71a955b..3227324cb 100644 --- a/spec/design/skel/Invocations_H.thy +++ b/spec/design/skel/Invocations_H.thy @@ -7,8 +7,8 @@ theory Invocations_H imports Structures_H - "./$L4V_ARCH/ArchRetypeDecls_H" - "./$L4V_ARCH/ArchLabelFuns_H" + ArchRetypeDecls_H + ArchLabelFuns_H begin requalify_types (in Arch) copy_register_sets irqcontrol_invocation diff --git a/spec/design/skel/KernelInit_H.thy b/spec/design/skel/KernelInit_H.thy index 76dd27c06..490c64222 100644 --- a/spec/design/skel/KernelInit_H.thy +++ b/spec/design/skel/KernelInit_H.thy @@ -9,7 +9,7 @@ chapter "Initialisation" theory KernelInit_H imports KI_Decls_H - "./$L4V_ARCH/ArchRetype_H" + ArchRetype_H Retype_H Config_H Thread_H diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index 154d609b1..82a0ab755 100644 --- a/spec/design/skel/KernelStateData_H.thy +++ b/spec/design/skel/KernelStateData_H.thy @@ -14,8 +14,8 @@ theory KernelStateData_H imports PSpaceStruct_H Structures_H - "../machine/$L4V_ARCH/MachineOps" - "./$L4V_ARCH/ArchStateData_H" + MachineOps + ArchStateData_H begin context begin interpretation Arch . diff --git a/spec/design/skel/ObjectInstances_H.thy b/spec/design/skel/ObjectInstances_H.thy index a43aed001..c65ed3923 100644 --- a/spec/design/skel/ObjectInstances_H.thy +++ b/spec/design/skel/ObjectInstances_H.thy @@ -13,7 +13,7 @@ chapter "Storable Object Instances" theory ObjectInstances_H imports Structures_H - "./$L4V_ARCH/State_H" + State_H PSpaceStorable_H Config_H begin diff --git a/spec/design/skel/RISCV64/ArchFaultHandler_H.thy b/spec/design/skel/RISCV64/ArchFaultHandler_H.thy index 331c842ba..232190374 100644 --- a/spec/design/skel/RISCV64/ArchFaultHandler_H.thy +++ b/spec/design/skel/RISCV64/ArchFaultHandler_H.thy @@ -7,7 +7,7 @@ chapter "Fault Handlers" theory ArchFaultHandler_H -imports "../TCB_H" "../Structures_H" +imports TCB_H Structures_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchFault_H.thy b/spec/design/skel/RISCV64/ArchFault_H.thy index b43d5be28..0ec5f0a68 100644 --- a/spec/design/skel/RISCV64/ArchFault_H.thy +++ b/spec/design/skel/RISCV64/ArchFault_H.thy @@ -9,7 +9,7 @@ *) theory ArchFault_H -imports "../Types_H" +imports Types_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchHypervisor_H.thy b/spec/design/skel/RISCV64/ArchHypervisor_H.thy index a139ed22e..ab1c104c9 100644 --- a/spec/design/skel/RISCV64/ArchHypervisor_H.thy +++ b/spec/design/skel/RISCV64/ArchHypervisor_H.thy @@ -10,9 +10,9 @@ theory ArchHypervisor_H imports - "../CNode_H" - "../KI_Decls_H" - "../InterruptDecls_H" + CNode_H + KI_Decls_H + InterruptDecls_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchIntermediate_H.thy b/spec/design/skel/RISCV64/ArchIntermediate_H.thy index dbcbd7ce3..82bc64f2b 100644 --- a/spec/design/skel/RISCV64/ArchIntermediate_H.thy +++ b/spec/design/skel/RISCV64/ArchIntermediate_H.thy @@ -7,7 +7,7 @@ chapter "Intermediate" theory ArchIntermediate_H -imports "../Intermediate_H" +imports Intermediate_H begin context Arch begin diff --git a/spec/design/skel/RISCV64/ArchInterruptDecls_H.thy b/spec/design/skel/RISCV64/ArchInterruptDecls_H.thy index 9b8e3d708..35a89aaa4 100644 --- a/spec/design/skel/RISCV64/ArchInterruptDecls_H.thy +++ b/spec/design/skel/RISCV64/ArchInterruptDecls_H.thy @@ -5,7 +5,7 @@ *) theory ArchInterruptDecls_H -imports "../RetypeDecls_H" "../CNode_H" +imports RetypeDecls_H CNode_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchInterrupt_H.thy b/spec/design/skel/RISCV64/ArchInterrupt_H.thy index 209d5276e..8a4d5e56c 100644 --- a/spec/design/skel/RISCV64/ArchInterrupt_H.thy +++ b/spec/design/skel/RISCV64/ArchInterrupt_H.thy @@ -6,9 +6,9 @@ theory ArchInterrupt_H imports - "../RetypeDecls_H" - "../CNode_H" - "../InterruptDecls_H" + RetypeDecls_H + CNode_H + InterruptDecls_H ArchInterruptDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy b/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy index cd16977fb..bae9fc2b0 100644 --- a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy +++ b/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy @@ -9,7 +9,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports "Word_Lib.Enumeration" - "../../machine/Setup_Locale" + Setup_Locale begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchLabelFuns_H.thy b/spec/design/skel/RISCV64/ArchLabelFuns_H.thy index 41c43dc8c..c0634387d 100644 --- a/spec/design/skel/RISCV64/ArchLabelFuns_H.thy +++ b/spec/design/skel/RISCV64/ArchLabelFuns_H.thy @@ -7,7 +7,7 @@ chapter "Architecture-specific Invocation Label Functions" theory ArchLabelFuns_H -imports "../InvocationLabels_H" +imports InvocationLabels_H begin text \ diff --git a/spec/design/skel/RISCV64/ArchObjInsts_H.thy b/spec/design/skel/RISCV64/ArchObjInsts_H.thy index 0b194d09f..43953fcee 100644 --- a/spec/design/skel/RISCV64/ArchObjInsts_H.thy +++ b/spec/design/skel/RISCV64/ArchObjInsts_H.thy @@ -13,8 +13,8 @@ chapter "Storable Arch Object Instances" theory ArchObjInsts_H imports ArchTypes_H - "../PSpaceStorable_H" - "../ObjectInstances_H" + PSpaceStorable_H + ObjectInstances_H begin qualify RISCV64_H (in Arch) diff --git a/spec/design/skel/RISCV64/ArchRetypeDecls_H.thy b/spec/design/skel/RISCV64/ArchRetypeDecls_H.thy index 005caf178..d6231de32 100644 --- a/spec/design/skel/RISCV64/ArchRetypeDecls_H.thy +++ b/spec/design/skel/RISCV64/ArchRetypeDecls_H.thy @@ -8,10 +8,10 @@ chapter "Retyping Objects" theory ArchRetypeDecls_H imports - "../FaultMonad_H" - "../EndpointDecls_H" - "../KernelInitMonad_H" - "../PSpaceFuns_H" + FaultMonad_H + EndpointDecls_H + KernelInitMonad_H + PSpaceFuns_H ArchObjInsts_H begin diff --git a/spec/design/skel/RISCV64/ArchRetype_H.thy b/spec/design/skel/RISCV64/ArchRetype_H.thy index b75b615b7..ff26de9ce 100644 --- a/spec/design/skel/RISCV64/ArchRetype_H.thy +++ b/spec/design/skel/RISCV64/ArchRetype_H.thy @@ -11,7 +11,7 @@ imports ArchRetypeDecls_H ArchVSpaceDecls_H Hardware_H - "../KI_Decls_H" + KI_Decls_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchStructures_H.thy b/spec/design/skel/RISCV64/ArchStructures_H.thy index e32ea5359..002c9174e 100644 --- a/spec/design/skel/RISCV64/ArchStructures_H.thy +++ b/spec/design/skel/RISCV64/ArchStructures_H.thy @@ -7,7 +7,7 @@ theory ArchStructures_H imports "Lib.Lib" - "../Types_H" + Types_H Hardware_H begin diff --git a/spec/design/skel/RISCV64/ArchTCB_H.thy b/spec/design/skel/RISCV64/ArchTCB_H.thy index dcc297d37..a32c25780 100644 --- a/spec/design/skel/RISCV64/ArchTCB_H.thy +++ b/spec/design/skel/RISCV64/ArchTCB_H.thy @@ -5,7 +5,7 @@ *) theory ArchTCB_H -imports "../TCBDecls_H" +imports TCBDecls_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchThreadDecls_H.thy b/spec/design/skel/RISCV64/ArchThreadDecls_H.thy index 7aac9d99a..dfc27dde0 100644 --- a/spec/design/skel/RISCV64/ArchThreadDecls_H.thy +++ b/spec/design/skel/RISCV64/ArchThreadDecls_H.thy @@ -12,9 +12,9 @@ chapter "Function Declarations for Threads" theory ArchThreadDecls_H imports - "../Structures_H" - "../FaultMonad_H" - "../KernelInitMonad_H" + Structures_H + FaultMonad_H + KernelInitMonad_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchThread_H.thy b/spec/design/skel/RISCV64/ArchThread_H.thy index b1b1865b9..073b2ddd5 100644 --- a/spec/design/skel/RISCV64/ArchThread_H.thy +++ b/spec/design/skel/RISCV64/ArchThread_H.thy @@ -9,11 +9,10 @@ chapter "Threads" theory ArchThread_H imports ArchThreadDecls_H - "../TCBDecls_H" + TCBDecls_H ArchVSpaceDecls_H begin - context Arch begin global_naming RISCV64_H #INCLUDE_HASKELL SEL4/Kernel/Thread/RISCV64.hs CONTEXT RISCV64_H Arch=MachineOps ArchReg=MachineTypes bodies_only diff --git a/spec/design/skel/RISCV64/ArchVSpaceDecls_H.thy b/spec/design/skel/RISCV64/ArchVSpaceDecls_H.thy index 6de7628bc..b75eb06b1 100644 --- a/spec/design/skel/RISCV64/ArchVSpaceDecls_H.thy +++ b/spec/design/skel/RISCV64/ArchVSpaceDecls_H.thy @@ -7,7 +7,7 @@ chapter "Retyping Objects" theory ArchVSpaceDecls_H -imports ArchRetypeDecls_H "../InvocationLabels_H" +imports ArchRetypeDecls_H InvocationLabels_H begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchVSpace_H.thy b/spec/design/skel/RISCV64/ArchVSpace_H.thy index 16b621137..5baf29d51 100644 --- a/spec/design/skel/RISCV64/ArchVSpace_H.thy +++ b/spec/design/skel/RISCV64/ArchVSpace_H.thy @@ -10,9 +10,9 @@ theory ArchVSpace_H imports - "../CNode_H" - "../Untyped_H" - "../KI_Decls_H" + CNode_H + Untyped_H + KI_Decls_H ArchVSpaceDecls_H begin diff --git a/spec/design/skel/RISCV64/Arch_Structs_B.thy b/spec/design/skel/RISCV64/Arch_Structs_B.thy index 33194ddeb..d1ea2108b 100644 --- a/spec/design/skel/RISCV64/Arch_Structs_B.thy +++ b/spec/design/skel/RISCV64/Arch_Structs_B.thy @@ -9,7 +9,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports "../../../spec/machine/Setup_Locale" +imports Setup_Locale begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/Hardware_H.thy b/spec/design/skel/RISCV64/Hardware_H.thy index 5b8439bec..ed508c2ff 100644 --- a/spec/design/skel/RISCV64/Hardware_H.thy +++ b/spec/design/skel/RISCV64/Hardware_H.thy @@ -6,7 +6,7 @@ theory Hardware_H imports - "../../machine/RISCV64/MachineOps" + MachineOps State_H begin diff --git a/spec/design/skel/RISCV64/RegisterSet_H.thy b/spec/design/skel/RISCV64/RegisterSet_H.thy index 1fcf177a0..5d3a53042 100644 --- a/spec/design/skel/RISCV64/RegisterSet_H.thy +++ b/spec/design/skel/RISCV64/RegisterSet_H.thy @@ -9,7 +9,7 @@ chapter "Register Set" theory RegisterSet_H imports "Lib.HaskellLib_H" - "../../machine/RISCV64/MachineOps" + MachineOps begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RetypeDecls_H.thy b/spec/design/skel/RetypeDecls_H.thy index 67fcf5123..5685e8fcb 100644 --- a/spec/design/skel/RetypeDecls_H.thy +++ b/spec/design/skel/RetypeDecls_H.thy @@ -8,7 +8,7 @@ chapter "Function Declarations for Retyping Objects" theory RetypeDecls_H imports - "./$L4V_ARCH/ArchRetypeDecls_H" + ArchRetypeDecls_H Structures_H FaultMonad_H Invocations_H diff --git a/spec/design/skel/Structures_H.thy b/spec/design/skel/Structures_H.thy index cdc079639..e502ad8f9 100644 --- a/spec/design/skel/Structures_H.thy +++ b/spec/design/skel/Structures_H.thy @@ -13,10 +13,10 @@ chapter "Kernel Data Structures" theory Structures_H imports Config_H - "./$L4V_ARCH/State_H" + State_H Fault_H Types_H - "./$L4V_ARCH/ArchStructures_H" + ArchStructures_H begin context begin interpretation Arch . diff --git a/spec/design/skel/TCB_H.thy b/spec/design/skel/TCB_H.thy index a6514ff2b..a78eb5be3 100644 --- a/spec/design/skel/TCB_H.thy +++ b/spec/design/skel/TCB_H.thy @@ -12,7 +12,7 @@ imports TCBDecls_H CNode_H VSpace_H - "./$L4V_ARCH/ArchTCB_H" + ArchTCB_H begin context begin interpretation Arch . diff --git a/spec/design/skel/ThreadDecls_H.thy b/spec/design/skel/ThreadDecls_H.thy index 7cb585286..3514987a0 100644 --- a/spec/design/skel/ThreadDecls_H.thy +++ b/spec/design/skel/ThreadDecls_H.thy @@ -11,7 +11,7 @@ imports Structures_H FaultMonad_H KernelInitMonad_H - "./$L4V_ARCH/ArchThreadDecls_H" + ArchThreadDecls_H begin #INCLUDE_HASKELL SEL4/Kernel/Thread.lhs decls_only NOT transferCapsToSlots diff --git a/spec/design/skel/Thread_H.thy b/spec/design/skel/Thread_H.thy index bb997c0a0..73cf00da4 100644 --- a/spec/design/skel/Thread_H.thy +++ b/spec/design/skel/Thread_H.thy @@ -10,7 +10,7 @@ theory Thread_H imports ThreadDecls_H CSpace_H - "./$L4V_ARCH/ArchThread_H" + ArchThread_H FaultHandler_H Config_H begin diff --git a/spec/design/skel/Types_H.thy b/spec/design/skel/Types_H.thy index dd9d48abd..720b60d79 100644 --- a/spec/design/skel/Types_H.thy +++ b/spec/design/skel/Types_H.thy @@ -12,9 +12,9 @@ chapter "Types visible in the API" theory Types_H imports - "./$L4V_ARCH/State_H" + State_H "Lib.Lib" - "./$L4V_ARCH/ArchTypes_H" + ArchTypes_H begin context begin interpretation Arch . diff --git a/spec/design/skel/Untyped_H.thy b/spec/design/skel/Untyped_H.thy index f0c141baa..44a6b16d7 100644 --- a/spec/design/skel/Untyped_H.thy +++ b/spec/design/skel/Untyped_H.thy @@ -14,7 +14,7 @@ imports Invocations_H InvocationLabels_H Config_H - "../machine/MachineExports" + MachineExports begin context begin interpretation Arch . diff --git a/spec/design/skel/VSpace_H.thy b/spec/design/skel/VSpace_H.thy index e03bb456b..629bf91d6 100644 --- a/spec/design/skel/VSpace_H.thy +++ b/spec/design/skel/VSpace_H.thy @@ -11,7 +11,7 @@ theory VSpace_H imports CNode_H - "./$L4V_ARCH/ArchVSpace_H" + ArchVSpace_H KernelInitMonad_H begin diff --git a/spec/design/skel/X64/ArchFaultHandler_H.thy b/spec/design/skel/X64/ArchFaultHandler_H.thy index 95183fc60..f14a1ae5e 100644 --- a/spec/design/skel/X64/ArchFaultHandler_H.thy +++ b/spec/design/skel/X64/ArchFaultHandler_H.thy @@ -7,7 +7,7 @@ chapter "Fault Handlers" theory ArchFaultHandler_H -imports "../TCB_H" "../Structures_H" +imports TCB_H Structures_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchFault_H.thy b/spec/design/skel/X64/ArchFault_H.thy index e3ee8a819..b5337200f 100644 --- a/spec/design/skel/X64/ArchFault_H.thy +++ b/spec/design/skel/X64/ArchFault_H.thy @@ -9,7 +9,7 @@ *) theory ArchFault_H -imports "../Types_H" +imports Types_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchHook_H.thy b/spec/design/skel/X64/ArchHook_H.thy index ccdc1c195..0f41142fc 100644 --- a/spec/design/skel/X64/ArchHook_H.thy +++ b/spec/design/skel/X64/ArchHook_H.thy @@ -7,7 +7,7 @@ chapter "ArchHook" theory ArchHook_H -imports "../KernelStateData_H" +imports KernelStateData_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchHypervisor_H.thy b/spec/design/skel/X64/ArchHypervisor_H.thy index 10b37e1f8..380ea0088 100644 --- a/spec/design/skel/X64/ArchHypervisor_H.thy +++ b/spec/design/skel/X64/ArchHypervisor_H.thy @@ -10,12 +10,12 @@ theory ArchHypervisor_H imports - "../CNode_H" - "../KI_Decls_H" - "../InterruptDecls_H" + CNode_H + KI_Decls_H + InterruptDecls_H begin -context Arch begin global_naming X64_H +context Arch begin global_naming X64_H #INCLUDE_HASKELL SEL4/Kernel/Hypervisor/X64.lhs Arch= CONTEXT X64_H decls_only ArchInv= ArchLabels= #INCLUDE_HASKELL SEL4/Kernel/Hypervisor/X64.lhs Arch= CONTEXT X64_H bodies_only ArchInv= ArchLabels= diff --git a/spec/design/skel/X64/ArchIntermediate_H.thy b/spec/design/skel/X64/ArchIntermediate_H.thy index 6d72b5f76..caa7a14ed 100644 --- a/spec/design/skel/X64/ArchIntermediate_H.thy +++ b/spec/design/skel/X64/ArchIntermediate_H.thy @@ -7,7 +7,7 @@ chapter "Intermediate" theory ArchIntermediate_H -imports "../Intermediate_H" +imports Intermediate_H begin context Arch begin diff --git a/spec/design/skel/X64/ArchInterruptDecls_H.thy b/spec/design/skel/X64/ArchInterruptDecls_H.thy index 62a39dbee..c34fbd11a 100644 --- a/spec/design/skel/X64/ArchInterruptDecls_H.thy +++ b/spec/design/skel/X64/ArchInterruptDecls_H.thy @@ -5,7 +5,7 @@ *) theory ArchInterruptDecls_H -imports "../RetypeDecls_H" "../CNode_H" +imports RetypeDecls_H CNode_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchInterrupt_H.thy b/spec/design/skel/X64/ArchInterrupt_H.thy index 22ff36756..06d44aa8c 100644 --- a/spec/design/skel/X64/ArchInterrupt_H.thy +++ b/spec/design/skel/X64/ArchInterrupt_H.thy @@ -6,9 +6,9 @@ theory ArchInterrupt_H imports - "../RetypeDecls_H" - "../CNode_H" - "../InterruptDecls_H" + RetypeDecls_H + CNode_H + InterruptDecls_H ArchInterruptDecls_H ArchHypervisor_H begin diff --git a/spec/design/skel/X64/ArchInvocationLabels_H.thy b/spec/design/skel/X64/ArchInvocationLabels_H.thy index 8304a9dce..c967f7f16 100644 --- a/spec/design/skel/X64/ArchInvocationLabels_H.thy +++ b/spec/design/skel/X64/ArchInvocationLabels_H.thy @@ -9,7 +9,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports "Word_Lib.Enumeration" - "../../machine/Setup_Locale" + Setup_Locale begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchLabelFuns_H.thy b/spec/design/skel/X64/ArchLabelFuns_H.thy index 7b575d56f..de0c77616 100644 --- a/spec/design/skel/X64/ArchLabelFuns_H.thy +++ b/spec/design/skel/X64/ArchLabelFuns_H.thy @@ -7,7 +7,7 @@ chapter "Architecture-specific Invocation Label Functions" theory ArchLabelFuns_H -imports "../InvocationLabels_H" +imports InvocationLabels_H begin text \ diff --git a/spec/design/skel/X64/ArchObjInsts_H.thy b/spec/design/skel/X64/ArchObjInsts_H.thy index bfcd5eff5..73dd9d252 100644 --- a/spec/design/skel/X64/ArchObjInsts_H.thy +++ b/spec/design/skel/X64/ArchObjInsts_H.thy @@ -13,8 +13,8 @@ chapter "Storable Arch Object Instances" theory ArchObjInsts_H imports ArchTypes_H - "../PSpaceStorable_H" - "../ObjectInstances_H" + PSpaceStorable_H + ObjectInstances_H begin qualify X64_H (in Arch) diff --git a/spec/design/skel/X64/ArchRetypeDecls_H.thy b/spec/design/skel/X64/ArchRetypeDecls_H.thy index 301249d59..c7c2f0b36 100644 --- a/spec/design/skel/X64/ArchRetypeDecls_H.thy +++ b/spec/design/skel/X64/ArchRetypeDecls_H.thy @@ -8,10 +8,10 @@ chapter "Retyping Objects" theory ArchRetypeDecls_H imports - "../FaultMonad_H" - "../EndpointDecls_H" - "../KernelInitMonad_H" - "../PSpaceFuns_H" + FaultMonad_H + EndpointDecls_H + KernelInitMonad_H + PSpaceFuns_H ArchObjInsts_H begin diff --git a/spec/design/skel/X64/ArchRetype_H.thy b/spec/design/skel/X64/ArchRetype_H.thy index c8f8bb98f..57e6933c3 100644 --- a/spec/design/skel/X64/ArchRetype_H.thy +++ b/spec/design/skel/X64/ArchRetype_H.thy @@ -11,7 +11,7 @@ imports ArchRetypeDecls_H ArchVSpaceDecls_H Hardware_H - "../KI_Decls_H" + KI_Decls_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchStructures_H.thy b/spec/design/skel/X64/ArchStructures_H.thy index 8e8621d24..3d754c923 100644 --- a/spec/design/skel/X64/ArchStructures_H.thy +++ b/spec/design/skel/X64/ArchStructures_H.thy @@ -7,7 +7,7 @@ theory ArchStructures_H imports "Lib.Lib" - "../Types_H" + Types_H Hardware_H begin diff --git a/spec/design/skel/X64/ArchTCB_H.thy b/spec/design/skel/X64/ArchTCB_H.thy index 64db194e3..9027eec60 100644 --- a/spec/design/skel/X64/ArchTCB_H.thy +++ b/spec/design/skel/X64/ArchTCB_H.thy @@ -5,7 +5,7 @@ *) theory ArchTCB_H -imports "../TCBDecls_H" +imports TCBDecls_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchThreadDecls_H.thy b/spec/design/skel/X64/ArchThreadDecls_H.thy index b33283adb..9d9bdccfa 100644 --- a/spec/design/skel/X64/ArchThreadDecls_H.thy +++ b/spec/design/skel/X64/ArchThreadDecls_H.thy @@ -12,9 +12,9 @@ chapter "Function Declarations for Threads" theory ArchThreadDecls_H imports - "../Structures_H" - "../FaultMonad_H" - "../KernelInitMonad_H" + Structures_H + FaultMonad_H + KernelInitMonad_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchThread_H.thy b/spec/design/skel/X64/ArchThread_H.thy index f10e101d5..02719eca2 100644 --- a/spec/design/skel/X64/ArchThread_H.thy +++ b/spec/design/skel/X64/ArchThread_H.thy @@ -9,7 +9,7 @@ chapter "Threads" theory ArchThread_H imports ArchThreadDecls_H - "../TCBDecls_H" + TCBDecls_H ArchVSpaceDecls_H begin diff --git a/spec/design/skel/X64/ArchVSpaceDecls_H.thy b/spec/design/skel/X64/ArchVSpaceDecls_H.thy index 0bcbe0fe0..a7ce162ad 100644 --- a/spec/design/skel/X64/ArchVSpaceDecls_H.thy +++ b/spec/design/skel/X64/ArchVSpaceDecls_H.thy @@ -7,7 +7,7 @@ chapter "Retyping Objects" theory ArchVSpaceDecls_H -imports ArchRetypeDecls_H "../InvocationLabels_H" +imports ArchRetypeDecls_H InvocationLabels_H begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchVSpace_H.thy b/spec/design/skel/X64/ArchVSpace_H.thy index 40bd8d44d..b754ef75e 100644 --- a/spec/design/skel/X64/ArchVSpace_H.thy +++ b/spec/design/skel/X64/ArchVSpace_H.thy @@ -10,9 +10,9 @@ theory ArchVSpace_H imports - "../CNode_H" - "../Untyped_H" - "../KI_Decls_H" + CNode_H + Untyped_H + KI_Decls_H ArchVSpaceDecls_H begin diff --git a/spec/design/skel/X64/Arch_Structs_B.thy b/spec/design/skel/X64/Arch_Structs_B.thy index 8f638e3fb..8c368218b 100644 --- a/spec/design/skel/X64/Arch_Structs_B.thy +++ b/spec/design/skel/X64/Arch_Structs_B.thy @@ -9,7 +9,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports Main "../../../spec/machine/Setup_Locale" +imports Main Setup_Locale begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/Hardware_H.thy b/spec/design/skel/X64/Hardware_H.thy index fe54fa347..7ff459172 100644 --- a/spec/design/skel/X64/Hardware_H.thy +++ b/spec/design/skel/X64/Hardware_H.thy @@ -6,7 +6,7 @@ theory Hardware_H imports - "../../machine/X64/MachineOps" + MachineOps State_H begin diff --git a/spec/design/skel/X64/RegisterSet_H.thy b/spec/design/skel/X64/RegisterSet_H.thy index f1431061d..eac65549f 100644 --- a/spec/design/skel/X64/RegisterSet_H.thy +++ b/spec/design/skel/X64/RegisterSet_H.thy @@ -9,7 +9,7 @@ chapter "Register Set" theory RegisterSet_H imports "Lib.HaskellLib_H" - "../../machine/X64/MachineOps" + MachineOps begin context Arch begin global_naming X64_H diff --git a/spec/machine/ARM/MachineOps.thy b/spec/machine/ARM/MachineOps.thy index eee6fb5a4..0d2b48094 100644 --- a/spec/machine/ARM/MachineOps.thy +++ b/spec/machine/ARM/MachineOps.thy @@ -8,7 +8,7 @@ chapter "Machine Operations" theory MachineOps imports - "../MachineMonad" + MachineMonad begin section "Wrapping and Lifting Machine Operations" diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy index 933a7eb5a..5653f432a 100644 --- a/spec/machine/ARM/Platform.thy +++ b/spec/machine/ARM/Platform.thy @@ -11,7 +11,7 @@ imports "Lib.Defs" "Lib.Lib" "Word_Lib.WordSetup" - "../Setup_Locale" + Setup_Locale begin context Arch begin global_naming ARM diff --git a/spec/machine/ARM_HYP/MachineOps.thy b/spec/machine/ARM_HYP/MachineOps.thy index 536c07403..2ab6317fa 100644 --- a/spec/machine/ARM_HYP/MachineOps.thy +++ b/spec/machine/ARM_HYP/MachineOps.thy @@ -8,7 +8,7 @@ chapter "Machine Operations" theory MachineOps imports - "../MachineMonad" + MachineMonad begin section "Wrapping and Lifting Machine Operations" diff --git a/spec/machine/ARM_HYP/Platform.thy b/spec/machine/ARM_HYP/Platform.thy index dc3a30158..4f2918a09 100644 --- a/spec/machine/ARM_HYP/Platform.thy +++ b/spec/machine/ARM_HYP/Platform.thy @@ -11,7 +11,7 @@ imports "Lib.Defs" "Lib.Lib" "Word_Lib.WordSetup" - "../Setup_Locale" + Setup_Locale begin context Arch begin global_naming ARM_HYP diff --git a/spec/machine/MachineExports.thy b/spec/machine/MachineExports.thy index 5873025e4..d91b8d0eb 100644 --- a/spec/machine/MachineExports.thy +++ b/spec/machine/MachineExports.thy @@ -6,7 +6,7 @@ theory MachineExports -imports "./$L4V_ARCH/MachineOps" +imports MachineOps begin context begin interpretation Arch . diff --git a/spec/machine/MachineMonad.thy b/spec/machine/MachineMonad.thy index aeb3ff72c..d50a1fcdf 100644 --- a/spec/machine/MachineMonad.thy +++ b/spec/machine/MachineMonad.thy @@ -6,7 +6,7 @@ theory MachineMonad -imports "./$L4V_ARCH/MachineTypes" +imports MachineTypes begin context begin interpretation Arch . diff --git a/spec/machine/RISCV64/MachineOps.thy b/spec/machine/RISCV64/MachineOps.thy index 4c3e88959..a48560d6b 100644 --- a/spec/machine/RISCV64/MachineOps.thy +++ b/spec/machine/RISCV64/MachineOps.thy @@ -10,7 +10,7 @@ theory MachineOps imports "Word_Lib.WordSetup" "Lib.NonDetMonad" - "../MachineMonad" + MachineMonad begin section "Wrapping and Lifting Machine Operations" diff --git a/spec/machine/RISCV64/Platform.thy b/spec/machine/RISCV64/Platform.thy index 9869993b6..274b68256 100644 --- a/spec/machine/RISCV64/Platform.thy +++ b/spec/machine/RISCV64/Platform.thy @@ -11,7 +11,7 @@ imports "Lib.Lib" "Word_Lib.Word_Enum" "Lib.Defs" - "../Setup_Locale" + Setup_Locale begin context Arch begin global_naming RISCV64 diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy index d0bbcbe99..86a391219 100644 --- a/spec/machine/X64/MachineOps.thy +++ b/spec/machine/X64/MachineOps.thy @@ -10,7 +10,7 @@ theory MachineOps imports "Word_Lib.WordSetup" "Lib.NonDetMonad" - "../MachineMonad" + MachineMonad begin section "Wrapping and Lifting Machine Operations" diff --git a/spec/machine/X64/Platform.thy b/spec/machine/X64/Platform.thy index 41751c028..40eed0844 100644 --- a/spec/machine/X64/Platform.thy +++ b/spec/machine/X64/Platform.thy @@ -11,7 +11,7 @@ imports "Lib.Lib" "Word_Lib.Word_Enum" "Lib.Defs" - "../Setup_Locale" + Setup_Locale begin context Arch begin global_naming X64 diff --git a/tools/asmrefine/CommonOps.thy b/tools/asmrefine/CommonOps.thy index ca99fb28b..8eeb6124e 100644 --- a/tools/asmrefine/CommonOps.thy +++ b/tools/asmrefine/CommonOps.thy @@ -5,10 +5,10 @@ *) theory CommonOps - -imports "CLib.CTranslationNICTA" - "GlobalsSwap" - "$L4V_ARCH/ArchSetup" +imports + "CLib.CTranslationNICTA" + GlobalsSwap + ArchSetup begin text \Additional constants needed to make conversion to and from the graph lang easy\ diff --git a/tools/c-parser/CProof.thy b/tools/c-parser/CProof.thy index 21514f883..50a2c38cf 100644 --- a/tools/c-parser/CProof.thy +++ b/tools/c-parser/CProof.thy @@ -6,10 +6,10 @@ theory CProof imports - "umm_heap/SepFrame" + SepFrame "Simpl-VCG.Vcg" - "umm_heap/StructSupport" - "umm_heap/ArrayAssertion" + StructSupport + ArrayAssertion begin (* name generation is the only thing this theory wants, but that diff --git a/tools/c-parser/Simpl/Simpl.thy b/tools/c-parser/Simpl/Simpl.thy index 51eb7e213..285ec17a5 100644 --- a/tools/c-parser/Simpl/Simpl.thy +++ b/tools/c-parser/Simpl/Simpl.thy @@ -30,15 +30,15 @@ imports StateSpace AlternativeSmallStep SyntaxTest - "ex/VcgEx" - "ex/VcgExSP" - "ex/VcgExTotal" - "ex/Quicksort" - "ex/XVcgEx" - "ex/ProcParEx" - "ex/ProcParExSP" - "ex/ClosureEx" - "ex/ComposeEx" + "VcgEx" + "VcgExSP" + "VcgExTotal" + "Quicksort" + "XVcgEx" + "ProcParEx" + "ProcParExSP" + "ClosureEx" + "ComposeEx" UserGuide begin end diff --git a/tools/c-parser/Simpl/ex/Closure.thy b/tools/c-parser/Simpl/ex/Closure.thy index edbdd34e7..6b8493a4b 100644 --- a/tools/c-parser/Simpl/ex/Closure.thy +++ b/tools/c-parser/Simpl/ex/Closure.thy @@ -29,7 +29,7 @@ USA section "Experiments with Closures" theory Closure -imports "../Hoare" +imports Hoare begin diff --git a/tools/c-parser/Simpl/ex/ClosureEx.thy b/tools/c-parser/Simpl/ex/ClosureEx.thy index 2ec61f548..90ef96b38 100644 --- a/tools/c-parser/Simpl/ex/ClosureEx.thy +++ b/tools/c-parser/Simpl/ex/ClosureEx.thy @@ -27,7 +27,7 @@ USA *) theory ClosureEx -imports "../Vcg" "../Simpl_Heap" Closure +imports Vcg Simpl_Heap Closure begin diff --git a/tools/c-parser/Simpl/ex/Compose.thy b/tools/c-parser/Simpl/ex/Compose.thy index fad29c886..70c2a5308 100644 --- a/tools/c-parser/Simpl/ex/Compose.thy +++ b/tools/c-parser/Simpl/ex/Compose.thy @@ -29,7 +29,7 @@ USA section "Experiments on State Composition" -theory Compose imports "../HoareTotalProps" begin +theory Compose imports HoareTotalProps begin text \ We develop some theory to support state-space modular development of programs. diff --git a/tools/c-parser/Simpl/ex/ComposeEx.thy b/tools/c-parser/Simpl/ex/ComposeEx.thy index 481992baf..58f225fb2 100644 --- a/tools/c-parser/Simpl/ex/ComposeEx.thy +++ b/tools/c-parser/Simpl/ex/ComposeEx.thy @@ -25,7 +25,7 @@ License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -theory ComposeEx imports Compose "../Vcg" "../HeapList" begin +theory ComposeEx imports Compose Vcg HeapList begin record globals_list = diff --git a/tools/c-parser/Simpl/ex/ProcParEx.thy b/tools/c-parser/Simpl/ex/ProcParEx.thy index 4e8bced61..3dd01a32b 100644 --- a/tools/c-parser/Simpl/ex/ProcParEx.thy +++ b/tools/c-parser/Simpl/ex/ProcParEx.thy @@ -28,7 +28,7 @@ USA section "Examples for Procedures as Parameters" -theory ProcParEx imports "../Vcg" begin +theory ProcParEx imports Vcg begin lemma DynProcProcPar': diff --git a/tools/c-parser/Simpl/ex/ProcParExSP.thy b/tools/c-parser/Simpl/ex/ProcParExSP.thy index 6688268a4..3d02d88c2 100644 --- a/tools/c-parser/Simpl/ex/ProcParExSP.thy +++ b/tools/c-parser/Simpl/ex/ProcParExSP.thy @@ -27,7 +27,7 @@ USA *) section "Examples for Procedures as Parameters using Statespaces" -theory ProcParExSP imports "../Vcg" begin +theory ProcParExSP imports Vcg begin lemma DynProcProcPar': diff --git a/tools/c-parser/Simpl/ex/Quicksort.thy b/tools/c-parser/Simpl/ex/Quicksort.thy index d32413428..b6c191722 100644 --- a/tools/c-parser/Simpl/ex/Quicksort.thy +++ b/tools/c-parser/Simpl/ex/Quicksort.thy @@ -29,7 +29,7 @@ USA section "Example: Quicksort on Heap Lists" theory Quicksort -imports "../Vcg" "../HeapList" "HOL-Library.Permutation" +imports Vcg HeapList "HOL-Library.Permutation" begin record globals_heap = diff --git a/tools/c-parser/Simpl/ex/VcgEx.thy b/tools/c-parser/Simpl/ex/VcgEx.thy index 4eaa44579..c290dad0a 100644 --- a/tools/c-parser/Simpl/ex/VcgEx.thy +++ b/tools/c-parser/Simpl/ex/VcgEx.thy @@ -28,7 +28,7 @@ USA section \Examples using the Verification Environment\ -theory VcgEx imports "../HeapList" "../Vcg" begin +theory VcgEx imports HeapList Vcg begin text \Some examples, especially the single-step Isar proofs are taken from \texttt{HOL/Isar\_examples/HoareEx.thy}. diff --git a/tools/c-parser/Simpl/ex/VcgExSP.thy b/tools/c-parser/Simpl/ex/VcgExSP.thy index 448b2bfbf..64bcf3779 100644 --- a/tools/c-parser/Simpl/ex/VcgExSP.thy +++ b/tools/c-parser/Simpl/ex/VcgExSP.thy @@ -28,7 +28,7 @@ USA section \Examples using Statespaces\ -theory VcgExSP imports "../HeapList" "../Vcg" begin +theory VcgExSP imports HeapList Vcg begin subsection \State Spaces\ diff --git a/tools/c-parser/Simpl/ex/VcgExTotal.thy b/tools/c-parser/Simpl/ex/VcgExTotal.thy index 1732e5754..bab8a30b2 100644 --- a/tools/c-parser/Simpl/ex/VcgExTotal.thy +++ b/tools/c-parser/Simpl/ex/VcgExTotal.thy @@ -28,7 +28,7 @@ USA section \Examples for Total Correctness\ -theory VcgExTotal imports "../HeapList" "../Vcg" begin +theory VcgExTotal imports HeapList Vcg begin record 'g vars = "'g state" + A_' :: nat diff --git a/tools/c-parser/Simpl/ex/XVcgEx.thy b/tools/c-parser/Simpl/ex/XVcgEx.thy index 0d6ae7ebf..4cd3fcbfd 100644 --- a/tools/c-parser/Simpl/ex/XVcgEx.thy +++ b/tools/c-parser/Simpl/ex/XVcgEx.thy @@ -29,7 +29,7 @@ USA section "Examples for Parallel Assignments" theory XVcgEx -imports "../XVcg" +imports XVcg begin diff --git a/tools/c-parser/testfiles/factorial.thy b/tools/c-parser/testfiles/factorial.thy index 48d5ccb55..57c1cd779 100644 --- a/tools/c-parser/testfiles/factorial.thy +++ b/tools/c-parser/testfiles/factorial.thy @@ -5,7 +5,7 @@ *) theory factorial -imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords" +imports "CParser.CTranslation" MachineWords begin declare hrs_simps [simp add] diff --git a/tools/c-parser/testfiles/kmalloc.thy b/tools/c-parser/testfiles/kmalloc.thy index 7313b9dad..0dbc3bb48 100644 --- a/tools/c-parser/testfiles/kmalloc.thy +++ b/tools/c-parser/testfiles/kmalloc.thy @@ -5,7 +5,7 @@ *) theory kmalloc -imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords" +imports "CParser.CTranslation" MachineWords begin (* no proof here, just testing the parser *) diff --git a/tools/c-parser/testfiles/list_reverse.thy b/tools/c-parser/testfiles/list_reverse.thy index 9ac0f245f..561140de2 100644 --- a/tools/c-parser/testfiles/list_reverse.thy +++ b/tools/c-parser/testfiles/list_reverse.thy @@ -5,7 +5,7 @@ *) theory list_reverse -imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords" +imports "CParser.CTranslation" MachineWords begin declare hrs_simps [simp add] diff --git a/tools/c-parser/testfiles/list_reverse_norm.thy b/tools/c-parser/testfiles/list_reverse_norm.thy index dcba63d3f..fa4023a87 100644 --- a/tools/c-parser/testfiles/list_reverse_norm.thy +++ b/tools/c-parser/testfiles/list_reverse_norm.thy @@ -5,7 +5,7 @@ *) theory list_reverse_norm -imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords" +imports "CParser.CTranslation" MachineWords begin declare sep_conj_ac [simp add] diff --git a/tools/c-parser/umm_heap/ARM/ArchArraysMemInstance.thy b/tools/c-parser/umm_heap/ARM/ArchArraysMemInstance.thy index 974352e48..7b6efabef 100644 --- a/tools/c-parser/umm_heap/ARM/ArchArraysMemInstance.thy +++ b/tools/c-parser/umm_heap/ARM/ArchArraysMemInstance.thy @@ -5,7 +5,7 @@ *) theory ArchArraysMemInstance -imports "../ArraysMemInstance" +imports ArraysMemInstance begin (* Showing arrays are in mem_type requires maximum sizes for objects, diff --git a/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy index 0d73c6377..92a20f552 100644 --- a/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy @@ -5,7 +5,7 @@ *) theory Word_Mem_Encoding - imports "../Vanilla32_Preliminaries" + imports Vanilla32_Preliminaries begin (* Little-endian encoding *) diff --git a/tools/c-parser/umm_heap/ARM_HYP/ArchArraysMemInstance.thy b/tools/c-parser/umm_heap/ARM_HYP/ArchArraysMemInstance.thy index 974352e48..7b6efabef 100644 --- a/tools/c-parser/umm_heap/ARM_HYP/ArchArraysMemInstance.thy +++ b/tools/c-parser/umm_heap/ARM_HYP/ArchArraysMemInstance.thy @@ -5,7 +5,7 @@ *) theory ArchArraysMemInstance -imports "../ArraysMemInstance" +imports ArraysMemInstance begin (* Showing arrays are in mem_type requires maximum sizes for objects, diff --git a/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy index 0d73c6377..92a20f552 100644 --- a/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/ARM_HYP/Word_Mem_Encoding.thy @@ -5,7 +5,7 @@ *) theory Word_Mem_Encoding - imports "../Vanilla32_Preliminaries" + imports Vanilla32_Preliminaries begin (* Little-endian encoding *) diff --git a/tools/c-parser/umm_heap/ArrayAssertion.thy b/tools/c-parser/umm_heap/ArrayAssertion.thy index 2520aa260..bd23510b9 100644 --- a/tools/c-parser/umm_heap/ArrayAssertion.thy +++ b/tools/c-parser/umm_heap/ArrayAssertion.thy @@ -9,7 +9,7 @@ theory ArrayAssertion imports - "$L4V_ARCH/ArchArraysMemInstance" + ArchArraysMemInstance "StructSupport" begin diff --git a/tools/c-parser/umm_heap/CTypesBase.thy b/tools/c-parser/umm_heap/CTypesBase.thy index d30debcde..5d6486dc8 100644 --- a/tools/c-parser/umm_heap/CTypesBase.thy +++ b/tools/c-parser/umm_heap/CTypesBase.thy @@ -13,7 +13,7 @@ theory CTypesBase imports - "./$L4V_ARCH/Addr_Type" + Addr_Type "HOL-Library.Prefix_Order" "Word_Lib.Signed_Words" begin diff --git a/tools/c-parser/umm_heap/RISCV64/ArchArraysMemInstance.thy b/tools/c-parser/umm_heap/RISCV64/ArchArraysMemInstance.thy index 6af98dc43..8eb2a8ffb 100644 --- a/tools/c-parser/umm_heap/RISCV64/ArchArraysMemInstance.thy +++ b/tools/c-parser/umm_heap/RISCV64/ArchArraysMemInstance.thy @@ -5,7 +5,7 @@ *) theory ArchArraysMemInstance -imports "../ArraysMemInstance" +imports ArraysMemInstance begin (* Showing arrays are in mem_type requires maximum sizes for objects, diff --git a/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy index 011f69caf..2190af612 100644 --- a/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/RISCV64/Word_Mem_Encoding.thy @@ -5,7 +5,7 @@ *) theory Word_Mem_Encoding - imports "../Vanilla32_Preliminaries" + imports Vanilla32_Preliminaries begin (* Little-endian encoding *) diff --git a/tools/c-parser/umm_heap/TypHeap.thy b/tools/c-parser/umm_heap/TypHeap.thy index 4fda6ea27..420dace34 100644 --- a/tools/c-parser/umm_heap/TypHeap.thy +++ b/tools/c-parser/umm_heap/TypHeap.thy @@ -9,7 +9,7 @@ theory TypHeap imports Vanilla32 - "$L4V_ARCH/ArchArraysMemInstance" + ArchArraysMemInstance HeapRawState MapExtraTrans begin diff --git a/tools/c-parser/umm_heap/Vanilla32.thy b/tools/c-parser/umm_heap/Vanilla32.thy index 7e2fd4e7d..f11104e0b 100644 --- a/tools/c-parser/umm_heap/Vanilla32.thy +++ b/tools/c-parser/umm_heap/Vanilla32.thy @@ -7,7 +7,7 @@ (* License: BSD, terms see file ./LICENSE *) theory Vanilla32 -imports "./$L4V_ARCH/Word_Mem_Encoding" "Word_Lib.Word_Lib" CTypes +imports Word_Mem_Encoding "Word_Lib.Word_Lib" CTypes begin diff --git a/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy b/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy index 6af98dc43..8eb2a8ffb 100644 --- a/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy +++ b/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy @@ -5,7 +5,7 @@ *) theory ArchArraysMemInstance -imports "../ArraysMemInstance" +imports ArraysMemInstance begin (* Showing arrays are in mem_type requires maximum sizes for objects, diff --git a/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy index 011f69caf..2190af612 100644 --- a/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy @@ -5,7 +5,7 @@ *) theory Word_Mem_Encoding - imports "../Vanilla32_Preliminaries" + imports Vanilla32_Preliminaries begin (* Little-endian encoding *)