ROOT
author nipkow
Mon, 31 Jul 2017 09:31:07 +0200
changeset 69872 8b31caaa4f06
parent 69869 0bba9c6b2a17
child 69884 8f40f652e71e
permissions -rw-r--r--
.

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"
    "../Public/Thys/BinHeap"
    "../Public/Thys/Skew_Heap_Analysis"
    "../Public/Thys/Splay_Tree_Analysis"
    "../Public/Thys/Pairing_Heap"

session Slides in Slides = "HOL-FDS17" +
  options [document_output = tex, document = pdf, names_short = true
      , document_variants = "document:handout"]
  theories[show_question_marks=false]
    Sorting_Slides
    Tree_Slides
    Search_Trees
    Tree23_Slides
    RBT_Slides
    Trie_Slides
    Leftist_Heap_Slides
    Braun_Tree_Slides
    Binomial_Tree_Slides
    Amor_Slides
    Skew_Heap_Slides
    Splay_Tree_Slides
    Pairing_Heap_Slides
  document_files
    "root.tex"
    "root_handout.tex"
    "main.tex"
    "prelude.tex"


session Slides_Heaps in Slides = "HOL-FDS17" +
  options [document_output = tex, document = pdf, names_short = true
      , document_variants = "partial"]
  theories[show_question_marks=false]
    Leftist_Heap_Slides
    Braun_Tree_Slides
    Binomial_Tree_Slides
  document_files
    "root_partial.tex"
    "prelude.tex"


session Amor_Slides in Slides = "HOL-FDS17" +
  options [document_output = tex, document = pdf, names_short = true
      , document_variants = "amor"]
  theories[show_question_marks=false]
    Amor_Slides
    Skew_Heap_Slides
    Splay_Tree_Slides
    Pairing_Heap_Slides
  document_files
    "root_amor.tex"
    "prelude.tex"

session MOD_Slides in Slides = "HOL-FDS17" +
  options [document_output = tex, document = pdf, names_short = true,
           document_variants = "mod"]
  theories[show_question_marks=false]
    MOD_Intro_Slides
    Time_Slides
    MOD_Tree_Slides
    Search_Trees
    MOD_Search_Trees
    Tree23_Slides
    RBT_Slides
    Leftist_Heap_Slides
    Braun_Tree_Slides
    Binomial_Tree_Slides
    Amor_Slides
    Skew_Heap_Slides
    Splay_Tree_Slides
    Pairing_Heap_Slides
  document_files
    "root_mod.tex"
    "prelude.tex"