Loading theory "Cmp" (required by "Tree_Set")
Loading theory "Less_False" (required by "Tree_Set" via "Set_by_Ordered" via "List_Ins_Del" via "Sorted_Less")
### theory "Less_False"
### 0.103s elapsed time, 0.284s cpu time, 0.000s GC time
Loading theory "Sorted_Less" (required by "Tree_Set" via "Set_by_Ordered" via "List_Ins_Del")
Found termination order: "length <*mlex*> {}"
### theory "Sorted_Less"
### 0.250s elapsed time, 0.500s cpu time, 0.000s GC time
Loading theory "List_Ins_Del" (required by "Tree_Set" via "Set_by_Ordered")
Found termination order: "length <*mlex*> {}"
### theory "Cmp"
### 0.587s elapsed time, 1.256s cpu time, 0.000s GC time
Loading theory "Tree" (required by "Tree_Set")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "List_Ins_Del"
### 0.575s elapsed time, 1.152s cpu time, 0.000s GC time
Loading theory "Set_by_Ordered" (required by "Tree_Set")
locale Set =
  fixes empty :: "'s" 
    and insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" 
    and delete :: "'a \<Rightarrow> 's \<Rightarrow> 's" 
    and isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool" 
    and set :: "'s \<Rightarrow> 'a set" 
    and invar :: "'s \<Rightarrow> bool" 
  assumes "Set empty insert delete isin set invar"
locale Set_by_Ordered =
  fixes empty :: "'t" 
    and insert :: "'a \<Rightarrow> 't \<Rightarrow> 't" 
    and delete :: "'a \<Rightarrow> 't \<Rightarrow> 't" 
    and isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool" 
    and inorder :: "'t \<Rightarrow> 'a list" 
    and inv :: "'t \<Rightarrow> bool" 
  assumes "Set_by_Ordered empty insert delete isin inorder inv"
### theory "Set_by_Ordered"
### 0.169s elapsed time, 0.340s cpu time, 0.000s GC time
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
class height = type +
  fixes height :: "'a \<Rightarrow> nat" 
instantiation
  tree :: (type) height
  height_tree == height :: 'a tree \<Rightarrow> nat
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
### theory "Tree"
### 4.153s elapsed time, 6.652s cpu time, 0.248s GC time
Loading theory "Tree_Set"
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
### Missing patterns in function definition:
### del_min \<langle>\<rangle> = undefined
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
### theory "Tree_Set"
### 1.297s elapsed time, 2.540s cpu time, 0.416s GC time
Loading theory "Random_BSTs"
### Ignoring duplicate rewrite rule:
### set_tree ?t1 = {} \<equiv> ?t1 = \<langle>\<rangle>
Found termination order: "length <*mlex*> {}"
consts
  lookup_cost :: "'a \<Rightarrow> 'a tree \<Rightarrow> nat"
### theory "Random_BSTs"
### 3.322s elapsed time, 4.148s cpu time, 0.000s GC time
isabelle document -c -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/document 2>&1
isabelle document -c -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/outline 2>&1
*** This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
***  restricted \write18 enabled.
*** entering extended mode
*** LaTeX2e <2016/02/01>
*** Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.
*** 
*** (./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
*** Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
*** (/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo)) (./isabelle.sty
*** (./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
*** Including comment 'isatagtheory' Including comment 'isadelimproof'
*** Including comment 'isatagproof' Including comment 'isadelimML'
*** Including comment 'isatagML' Including comment 'isadelimvisible'
*** Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
*** Excluding comment 'isataginvisible') (./isabelletags.sty
*** Including comment 'isadelimproof' Excluding comment 'isatagproof'
*** Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
*** ) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty)
*** (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
*** For additional information on amsmath, use the `?' option.
*** (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
*** (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
*** (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
*** (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
*** (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty)
*** (/usr/share/texlive/texmf-dist/tex/latex/was/upgreek.sty) (./pdfsetup.sty
*** (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
*** (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
*** (/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
*** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
*** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
*** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
*** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
*** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
*** (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
*** (/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
*** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
*** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
*** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
*** (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
*** (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))
*** 
*** Package hyperref Message: Driver (autodetected): hpdftex.
*** 
*** (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
*** (/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
*** No file root.aux.
*** (/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
*** [Loading MPS to PDF converter (version 2006.09.02).]
*** ) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
*** (/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
*** (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
*** (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) [1{/var/lib/texmf/fo
*** nts/map/pdftex/updmap/pdftex.map}] (./session.tex (./Tree.tex) (./Cmp.tex)
*** (./Less_False.tex) (./Sorted_Less.tex) (./List_Ins_Del.tex)
*** (./Set_by_Ordered.tex) (./Tree_Set.tex) (./Random_BSTs.tex))
*** No file root.bbl.
*** (./root.aux)
*** 
*** Package rerunfilecheck Warning: File `root.out' has changed.
*** (rerunfilecheck)                Rerun to get outlines right
*** (rerunfilecheck)                or use package `bookmark'.
*** 
***  )</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></us
*** r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/shar
*** e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texl
*** ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/tex
*** mf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist
*** /fonts/type1/public/amsfonts/cm/cmr17.pfb>
*** Output written on root.pdf (1 page, 64849 bytes).
*** Transcript written on root.log.
*** This is BibTeX, Version 0.99d (TeX Live 2015/Debian)
*** The top-level auxiliary file: root.aux
*** The style file: abbrv.bst
*** I found no \citation commands---while reading file root.aux
*** Database file #1: root.bib
*** (There was 1 error message)
*** Document preparation failure in directory '/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/outline'
*** 
*** Failed to build document "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Random_BSTs/outline.pdf"
*** Undefined fact: "path_len.simps" (line 603 of "~~/afp/thys/Random_BSTs/Random_BSTs.thy")
*** At command "text" (line 602 of "~~/afp/thys/Random_BSTs/Random_BSTs.thy")