ROOT
author nipkow
Fri, 23 Jun 2017 18:08:31 +0200
changeset 69808 74e6be42675e
child 69810 abb251c0c725
permissions -rw-r--r--
init

session "HOL-FDS17" = HOL +
  options [document = pdf, document_output="$THIS_DIR/FDS-generated"]
  theories [document = false]
    "~~/src/HOL/Library/Tree"
    "../Public/Thys/Tree_Additions"
    "~~/src/HOL/Data_Structures/Tree_Set"
    "~~/src/HOL/Data_Structures/Tree23_Set"
    "../Public/Thys/RBT_Set"
    "../Public/Thys/Trie2"
    "../Public/Thys/Leftist_Heap"
    "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
    "Slides/Tree_Notation"

session Slides in Slides = "HOL-FDS17" +
  options [document_output = tex, document = pdf, names_short = true]
  theories[show_question_marks=false]
    Sorting_Slides
    Tree_Slides
    Search_Trees
    Tree23_Slides
    RBT_Slides
    Trie_Slides
    Leftist_Heap_Slides
    Braun_Tree_Slides
  document_files
    "root.tex"
    "prelude.tex"