ROOT 837 Bytes
Newer Older
1
2
chapter AFP

nipkow's avatar
tuned    
nipkow committed
3
(* There must be one session with the name of the entry.
nipkow's avatar
tuned    
nipkow committed
4
5
6
7
8
   This session generates the web document.
   There may be further sessions.
   All sessions should be in group (AFP) - otherwise they are not
   run upon submission and by the later automatic regression tests.
   Every theory should be included in at least one of the sessions.
nipkow's avatar
tuned    
nipkow committed
9
10
*)

Gerwin Klein's avatar
Gerwin Klein committed
11
(* Session name, add to AFP group, list base session: *)
12
session "Example-Submission" (AFP) = HOL +
Gerwin Klein's avatar
Gerwin Klein committed
13
14

(* Timeout (in sec) in case of non-termination problems *)
15
  options [timeout = 600]
Gerwin Klein's avatar
Gerwin Klein committed
16
17
18
19
20
21
22
23
24

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

(* The top-level theories of the submission: *)
25
26
  theories
    Submission
Gerwin Klein's avatar
Gerwin Klein committed
27
    
wenzelm's avatar
wenzelm committed
28
(* Dependencies on document source files: *)
29
30
31
  document_files
    "root.bib"
    "root.tex"