ROOT
author nipkow
Fri, 23 Jun 2017 18:08:31 +0200
changeset 69808 74e6be42675e
child 69810 abb251c0c725
permissions -rw-r--r--
init
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69808
nipkow
parents:
diff changeset
     1
session "HOL-FDS17" = HOL +
nipkow
parents:
diff changeset
     2
  options [document = pdf, document_output="$THIS_DIR/FDS-generated"]
nipkow
parents:
diff changeset
     3
  theories [document = false]
nipkow
parents:
diff changeset
     4
    "~~/src/HOL/Library/Tree"
nipkow
parents:
diff changeset
     5
    "../Public/Thys/Tree_Additions"
nipkow
parents:
diff changeset
     6
    "~~/src/HOL/Data_Structures/Tree_Set"
nipkow
parents:
diff changeset
     7
    "~~/src/HOL/Data_Structures/Tree23_Set"
nipkow
parents:
diff changeset
     8
    "../Public/Thys/RBT_Set"
nipkow
parents:
diff changeset
     9
    "../Public/Thys/Trie2"
nipkow
parents:
diff changeset
    10
    "../Public/Thys/Leftist_Heap"
nipkow
parents:
diff changeset
    11
    "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
nipkow
parents:
diff changeset
    12
    "Slides/Tree_Notation"
nipkow
parents:
diff changeset
    13
nipkow
parents:
diff changeset
    14
session Slides in Slides = "HOL-FDS17" +
nipkow
parents:
diff changeset
    15
  options [document_output = tex, document = pdf, names_short = true]
nipkow
parents:
diff changeset
    16
  theories[show_question_marks=false]
nipkow
parents:
diff changeset
    17
    Sorting_Slides
nipkow
parents:
diff changeset
    18
    Tree_Slides
nipkow
parents:
diff changeset
    19
    Search_Trees
nipkow
parents:
diff changeset
    20
    Tree23_Slides
nipkow
parents:
diff changeset
    21
    RBT_Slides
nipkow
parents:
diff changeset
    22
    Trie_Slides
nipkow
parents:
diff changeset
    23
    Leftist_Heap_Slides
nipkow
parents:
diff changeset
    24
    Braun_Tree_Slides
nipkow
parents:
diff changeset
    25
  document_files
nipkow
parents:
diff changeset
    26
    "root.tex"
nipkow
parents:
diff changeset
    27
    "prelude.tex"