Commit 9beb9498 authored by Gerwin Klein's avatar Gerwin Klein
Browse files

Prettier example ROOT

parent c0d3a652c6d9
(* Session name, add to AFP group, list base session: *)
session "Example-Submission" (AFP) = HOL +
(* Timeout (in sec) in case of non-termination problems *)
options [timeout = 3600]
(* To suppress document generation of some theories: *)
(*
theories [document = false]
This_Theory
That_Theory
*)
(* The top-level theories of the submission: *)
theories
Submission
(* FIXME *)
(* to suppress document generation of some theories, use:
no_document use_thys ["This_Theory1", "This_Theory2"];
*)
(* for normal theory loading, use:
use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
(* Dependencies on non-Isabelle files: *)
files
"document/root.bib"
"document/root.tex"
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment