Quelle  ROOT

chapter AFP

session Huffman = HOL +
  options [timeout = 600]
  theories 
    Huffman
  document_files
    "forest-a.eps"
    "forest-a.pdf"
    "forest-a.svg"
    "forest-flat.eps"
    "forest-flat.pdf"
    "forest-flat.svg"
    "forest-optimal.eps"
    "forest-optimal.pdf"
    "forest-optimal.svg"
    "forest-splitLeaf-ab.eps"
    "forest-splitLeaf-ab.pdf"
    "forest-splitLeaf-ab.svg"
    "forest-uniteTrees-flat.eps"
    "forest-uniteTrees-flat.pdf"
    "forest-uniteTrees-flat.svg"
    "forest-uniteTrees.eps"
    "forest-uniteTrees.pdf"
    "forest-uniteTrees.svg"
    "forest-zigzag.eps"
    "forest-zigzag.pdf"
    "forest-zigzag.svg"
    "root.tex"
    "tree-abc-full.eps"
    "tree-abc-full.pdf"
    "tree-abc-full.svg"
    "tree-abc-non-full.eps"
    "tree-abc-non-full.pdf"
    "tree-abc-non-full.svg"
    "tree-abcd-balanced-weighted.eps"
    "tree-abcd-balanced-weighted.pdf"
    "tree-abcd-balanced-weighted.svg"
    "tree-abcd-balanced.eps"
    "tree-abcd-balanced.pdf"
    "tree-abcd-balanced.svg"
    "tree-abcd-non-prefix.eps"
    "tree-abcd-non-prefix.pdf"
    "tree-abcd-non-prefix.svg"
    "tree-abcd-unbalanced-weighted.eps"
    "tree-abcd-unbalanced-weighted.pdf"
    "tree-abcd-unbalanced-weighted.svg"
    "tree-abcd-unbalanced.eps"
    "tree-abcd-unbalanced.pdf"
    "tree-abcd-unbalanced.svg"
    "tree-huffman-splitLeaf-ab.eps"
    "tree-huffman-splitLeaf-ab.pdf"
    "tree-huffman-splitLeaf-ab.svg"
    "tree-minima-abcd.eps"
    "tree-minima-abcd.pdf"
    "tree-minima-abcd.svg"
    "tree-minima.eps"
    "tree-minima.pdf"
    "tree-minima.svg"
    "tree-optimal.eps"
    "tree-optimal.pdf"
    "tree-optimal.svg"
    "tree-prime-step1.eps"
    "tree-prime-step1.pdf"
    "tree-prime-step1.svg"
    "tree-prime-step2.eps"
    "tree-prime-step2.pdf"
    "tree-prime-step2.svg"
    "tree-prime-step3.eps"
    "tree-prime-step3.pdf"
    "tree-prime-step3.svg"
    "tree-prime-step4.eps"
    "tree-prime-step4.pdf"
    "tree-prime-step4.svg"
    "tree-prime-step5.eps"
    "tree-prime-step5.pdf"
    "tree-prime-step5.svg"
    "tree-sibling.eps"
    "tree-sibling.pdf"
    "tree-sibling.svg"
    "tree-splitLeaf-a.eps"
    "tree-splitLeaf-a.pdf"
    "tree-splitLeaf-a.svg"
    "tree-splitLeaf-ab.eps"
    "tree-splitLeaf-ab.pdf"
    "tree-splitLeaf-ab.svg"
    "tree-splitLeaf-abcd-aba.eps"
    "tree-splitLeaf-abcd-aba.pdf"
    "tree-splitLeaf-abcd-aba.svg"
    "tree-splitLeaf-abcd.eps"
    "tree-splitLeaf-abcd.pdf"
    "tree-splitLeaf-abcd.svg"
    "tree-splitLeaf-ba.eps"
    "tree-splitLeaf-ba.pdf"
    "tree-splitLeaf-ba.svg"
    "tree-splitLeaf-cd.eps"
    "tree-splitLeaf-cd.pdf"
    "tree-splitLeaf-cd.svg"
    "tree-suboptimal.eps"
    "tree-suboptimal.pdf"
    "tree-suboptimal.svg"
    "tree-w1-plus-w2.eps"
    "tree-w1-plus-w2.pdf"
    "tree-w1-plus-w2.svg"
    "tree-w1-w2-leaves.eps"
    "tree-w1-w2-leaves.pdf"
    "tree-w1-w2-leaves.svg"
    "tree-w1-w2.eps"
    "tree-w1-w2.pdf"
    "tree-w1-w2.svg"
    "tree-w1.eps"
    "tree-w1.pdf"
    "tree-w1.svg"
    "tree-w2.eps"
    "tree-w2.pdf"
    "tree-w2.svg"