ROOT 934 Bytes
Newer Older
1
2
chapter AFP

3
4
5
6
7
8
9
(* There must be one session with the (short) name of the entry.
   This session generates the web document and HTML files.

   It is strongly encouraged to have precisely one session, but it
   if needed, further sessions are permitted.

   All sessions must be in group (AFP) - otherwise they are not
nipkow's avatar
tuned    
nipkow committed
10
   run upon submission and by the later automatic regression tests.
11
12

   Every theory must be included in at least one of the sessions.
nipkow's avatar
tuned    
nipkow committed
13
14
*)

Gerwin Klein's avatar
Gerwin Klein committed
15
(* Session name, add to AFP group, list base session: *)
16
session "Example-Submission" (AFP) = HOL +
Gerwin Klein's avatar
Gerwin Klein committed
17
18

(* Timeout (in sec) in case of non-termination problems *)
19
  options [timeout = 600]
Gerwin Klein's avatar
Gerwin Klein committed
20
21
22
23
24
25
26
27
28

(* To suppress document generation of some theories: *)
(*
  theories [document = false]
    This_Theory
    That_Theory
*)

(* The top-level theories of the submission: *)
29
30
  theories
    Submission
31

wenzelm's avatar
wenzelm committed
32
(* Dependencies on document source files: *)
33
34
35
  document_files
    "root.bib"
    "root.tex"