adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: fix theory includes for arch-splitted WordSetup

This commit is contained in:
Joel Beeren 2016-05-20 12:31:10 +10:00
parent cc8d10a217
commit f52bc138b3
12 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/ARM/WordSetup.thy
View File

@ -12,7 +12,7 @@
theory WordSetup theory WordSetup
imports imports
"../Distinct_Prop" "../Distinct_Prop"
"Word_Lib/Word_Lemmas_32" "../Word_Lib/Word_Lemmas_32"
begin begin
(* Distinct_Prop lemmas that need word lemmas: *) (* Distinct_Prop lemmas that need word lemmas: *)

2
spec/ROOT
View File

@ -36,7 +36,7 @@ session ASpec in "abstract" = Word_Lib +
"../../lib/Lib" "../../lib/Lib"
"../../lib/Defs" "../../lib/Defs"
"../../lib/List_Lib" "../../lib/List_Lib"
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
theories theories
"Intro_Doc" "Intro_Doc"
"../../lib/Monad_WP/NonDetMonad" "../../lib/Monad_WP/NonDetMonad"

2
spec/capDL/Intents_D.thy
View File

@ -28,7 +28,7 @@
theory Intents_D theory Intents_D
imports imports
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
"../abstract/CapRights_A" "../abstract/CapRights_A"
begin begin

2
spec/cspec/KernelState_C.thy
View File

@ -10,7 +10,7 @@
theory KernelState_C theory KernelState_C
imports imports
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
"../../lib/BitFieldProofsLib" "../../lib/BitFieldProofsLib"
Kernel_C Kernel_C
Substitute Substitute

2
spec/machine/ARM/Platform.thy
View File

@ -14,7 +14,7 @@ theory Platform
imports imports
"../../../lib/Defs" "../../../lib/Defs"
"../../../lib/Lib" "../../../lib/Lib"
"../../../lib/WordSetup" "../../../lib/$L4V_ARCH/WordSetup"
Setup_Locale Setup_Locale
begin begin

2
spec/take-grant/System_S.thy
View File

@ -20,7 +20,7 @@
*) *)
theory System_S theory System_S
imports "../../lib/WordSetup" imports "../../lib/$L4V_ARCH/WordSetup"
begin begin
(* System entities: Definition of entities that constitute the system (* System entities: Definition of entities that constitute the system

2
tools/asmrefine/CommonOpsLemmas.thy
View File

@ -2,7 +2,7 @@ theory CommonOpsLemmas
imports imports
"CommonOps" "CommonOps"
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
begin begin
lemma fold_all_htd_updates': lemma fold_all_htd_updates':

2
tools/asmrefine/TailrecPre.thy
View File

@ -10,7 +10,7 @@
theory TailrecPre theory TailrecPre
imports imports
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
"../../lib/Lib" "../../lib/Lib"
begin begin

2
tools/autocorres/AbstractArrays.thy
View File

@ -11,7 +11,7 @@
theory AbstractArrays theory AbstractArrays
imports imports
"../../lib/TypHeapLib" "../../lib/TypHeapLib"
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
begin begin
(* (*

2
tools/autocorres/NonDetMonadEx.thy
View File

@ -14,7 +14,7 @@
theory NonDetMonadEx theory NonDetMonadEx
imports imports
"../../lib/WordSetup" "../../lib/$L4V_ARCH/WordSetup"
"../../lib/NonDetMonadLemmaBucket" "../../lib/NonDetMonadLemmaBucket"
"../../lib/Monad_WP/OptionMonadND" "../../lib/Monad_WP/OptionMonadND"
begin begin

2
tools/c-parser/PackedTypes.thy
View File

@ -9,7 +9,7 @@
*) *)
theory PackedTypes theory PackedTypes
imports "../../lib/WordSetup" CProof imports "../../lib/$L4V_ARCH/WordSetup" CProof
begin begin
section {* Underlying definitions for the class axioms *} section {* Underlying definitions for the class axioms *}

2
tools/c-parser/testfiles/ptr_modifies.thy
View File

@ -9,7 +9,7 @@
*) *)
theory ptr_modifies theory ptr_modifies
imports "../../../lib/WordSetup" "../CTranslation" imports "../../../lib/$L4V_ARCH/WordSetup" "../CTranslation"
begin begin
install_C_file "ptr_modifies.c" install_C_file "ptr_modifies.c"