diff --git a/spec/ROOT b/spec/ROOT index 2d97cdc05..7e2f5bbcd 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -36,7 +36,7 @@ session ASpec in "abstract" = Word_Lib + "../../lib/Lib" "../../lib/Defs" "../../lib/List_Lib" - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" theories "Intro_Doc" "../../lib/Monad_WP/NonDetMonad" diff --git a/spec/capDL/Intents_D.thy b/spec/capDL/Intents_D.thy index 8a3960e3a..38cd642b2 100644 --- a/spec/capDL/Intents_D.thy +++ b/spec/capDL/Intents_D.thy @@ -28,7 +28,7 @@ theory Intents_D imports - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" "../abstract/CapRights_A" begin diff --git a/spec/cspec/KernelState_C.thy b/spec/cspec/KernelState_C.thy index ade7fb0f3..32c33acdc 100644 --- a/spec/cspec/KernelState_C.thy +++ b/spec/cspec/KernelState_C.thy @@ -10,7 +10,7 @@ theory KernelState_C imports - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" "../../lib/BitFieldProofsLib" Kernel_C Substitute diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy index 9e6d83365..fd9c7f35d 100644 --- a/spec/machine/ARM/Platform.thy +++ b/spec/machine/ARM/Platform.thy @@ -14,7 +14,7 @@ theory Platform imports "../../../lib/Defs" "../../../lib/Lib" - "../../../lib/WordSetup" + "../../../lib/$L4V_ARCH/WordSetup" Setup_Locale begin diff --git a/spec/take-grant/System_S.thy b/spec/take-grant/System_S.thy index dce201599..4e2c9b573 100644 --- a/spec/take-grant/System_S.thy +++ b/spec/take-grant/System_S.thy @@ -20,7 +20,7 @@ *) theory System_S -imports "../../lib/WordSetup" +imports "../../lib/$L4V_ARCH/WordSetup" begin (* System entities: Definition of entities that constitute the system diff --git a/tools/asmrefine/CommonOpsLemmas.thy b/tools/asmrefine/CommonOpsLemmas.thy index 80e1a6bb9..f68938331 100644 --- a/tools/asmrefine/CommonOpsLemmas.thy +++ b/tools/asmrefine/CommonOpsLemmas.thy @@ -2,7 +2,7 @@ theory CommonOpsLemmas imports "CommonOps" - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" begin lemma fold_all_htd_updates': diff --git a/tools/asmrefine/TailrecPre.thy b/tools/asmrefine/TailrecPre.thy index 6958eb61e..389a1ecfa 100644 --- a/tools/asmrefine/TailrecPre.thy +++ b/tools/asmrefine/TailrecPre.thy @@ -10,7 +10,7 @@ theory TailrecPre imports - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" "../../lib/Lib" begin diff --git a/tools/autocorres/AbstractArrays.thy b/tools/autocorres/AbstractArrays.thy index 2b058e03a..d5edf8892 100644 --- a/tools/autocorres/AbstractArrays.thy +++ b/tools/autocorres/AbstractArrays.thy @@ -11,7 +11,7 @@ theory AbstractArrays imports "../../lib/TypHeapLib" - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" begin (* diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy index 6b359001b..e93cc72ba 100644 --- a/tools/autocorres/NonDetMonadEx.thy +++ b/tools/autocorres/NonDetMonadEx.thy @@ -14,7 +14,7 @@ theory NonDetMonadEx imports - "../../lib/WordSetup" + "../../lib/$L4V_ARCH/WordSetup" "../../lib/NonDetMonadLemmaBucket" "../../lib/Monad_WP/OptionMonadND" begin diff --git a/tools/c-parser/PackedTypes.thy b/tools/c-parser/PackedTypes.thy index 9f10cc9cd..4c4031af3 100644 --- a/tools/c-parser/PackedTypes.thy +++ b/tools/c-parser/PackedTypes.thy @@ -9,7 +9,7 @@ *) theory PackedTypes -imports "../../lib/WordSetup" CProof +imports "../../lib/$L4V_ARCH/WordSetup" CProof begin section {* Underlying definitions for the class axioms *} diff --git a/tools/c-parser/testfiles/ptr_modifies.thy b/tools/c-parser/testfiles/ptr_modifies.thy index 9e7f47c2d..63f081416 100644 --- a/tools/c-parser/testfiles/ptr_modifies.thy +++ b/tools/c-parser/testfiles/ptr_modifies.thy @@ -9,7 +9,7 @@ *) theory ptr_modifies -imports "../../../lib/WordSetup" "../CTranslation" +imports "../../../lib/$L4V_ARCH/WordSetup" "../CTranslation" begin install_C_file "ptr_modifies.c"