chapter AFP session "UPF-devel" (AFP) = HOL + description "The Unified Policy Framework (UPF) " options [timeout = 300] theories Monads UPF ServiceExample document_files "root.tex" "root.bib" "introduction.tex" "conclusion.tex" "example-intro.tex"