diff --git a/spec/ROOT b/spec/ROOT index afd66df05..f05baca97 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -110,6 +110,7 @@ session DSpec in capDL = Word_Lib + sessions ExecSpec ASpec + "HOL-Combinatorics" (* for Fun.swap *) theories Syscall_D diff --git a/spec/capDL/Types_D.thy b/spec/capDL/Types_D.thy index 91c5ec612..86d03959e 100644 --- a/spec/capDL/Types_D.thy +++ b/spec/capDL/Types_D.thy @@ -16,6 +16,7 @@ imports "ASpec.VMRights_A" Intents_D "Lib.SplitRule" + "HOL-Combinatorics.Transposition" (* for Fun.swap *) begin (* A hardware IRQ number. *)