1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7chapter Lib
8
9session Word_Lib (lib) = "HOL-Word" +
10  options [timeout = 150, document=pdf]
11  sessions
12    "HOL-Library"
13    "HOL-Eisbach"
14  directories  (* not in the AFP *)
15    "$L4V_ARCH"
16  theories
17    "Word_Lemmas_32"
18    "Word_Lemmas_64"
19  theories (* not in the AFP: *)
20    "Distinct_Prop"
21    "$L4V_ARCH/WordSetup"
22  document_files
23    "root.tex"
24