Loading theory "HOL-Algebra.Exponent" (required by "HOL-Algebra.Sylow")
Loading theory "HOL-Algebra.Congruence" (required by "HOL-Algebra.Galois_Connection" via "HOL-Algebra.Complete_Lattice" via "HOL-Algebra.Lattice" via "HOL-Algebra.Order")
### theory "HOL-Algebra.Exponent"
### 0.203s elapsed time, 0.404s cpu time, 0.000s GC time
### Metis: Unused theorems: "local.eeq_2"
locale equivalence
  fixes S :: "('a, 'b) eq_object_scheme"   (structure)
  assumes "equivalence S"
### theory "HOL-Algebra.Congruence"
### 1.161s elapsed time, 2.312s cpu time, 0.000s GC time
Loading theory "HOL-Algebra.Order" (required by "HOL-Algebra.Galois_Connection" via "HOL-Algebra.Complete_Lattice" via "HOL-Algebra.Lattice")
### theory "HOL-Algebra.Order"
### 0.408s elapsed time, 0.816s cpu time, 0.000s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "HOL-Algebra.Lattice" (unresolved "HOL-Algebra.Order")
*** Failed to load theory "HOL-Algebra.Complete_Lattice" (unresolved "HOL-Algebra.Lattice")
*** Failed to load theory "HOL-Algebra.Galois_Connection" (unresolved "HOL-Algebra.Complete_Lattice")
*** Failed to load theory "HOL-Algebra.Group" (unresolved "HOL-Algebra.Complete_Lattice")
*** Failed to load theory "HOL-Algebra.Bij" (unresolved "HOL-Algebra.Group")
*** Failed to load theory "HOL-Algebra.Coset" (unresolved "HOL-Algebra.Group")
*** Failed to load theory "HOL-Algebra.Sylow" (unresolved "HOL-Algebra.Coset")
*** Failed to load theory "HOL-Algebra.Divisibility" (unresolved "HOL-Algebra.Coset", "HOL-Algebra.Group")
*** Failed to load theory "HOL-Algebra.FiniteProduct" (unresolved "HOL-Algebra.Group")
*** Failed to load theory "HOL-Algebra.Ring" (unresolved "HOL-Algebra.FiniteProduct")
*** Failed to load theory "HOL-Algebra.AbelCoset" (unresolved "HOL-Algebra.Coset", "HOL-Algebra.Ring")
*** Failed to load theory "HOL-Algebra.Ideal" (unresolved "HOL-Algebra.AbelCoset", "HOL-Algebra.Ring")
*** Failed to load theory "HOL-Algebra.RingHom" (unresolved "HOL-Algebra.Ideal")
*** Failed to load theory "HOL-Algebra.QuotRing" (unresolved "HOL-Algebra.RingHom")
*** Failed to load theory "HOL-Algebra.Module" (unresolved "HOL-Algebra.Ring")
*** Failed to load theory "HOL-Algebra.UnivPoly" (unresolved "HOL-Algebra.Module", "HOL-Algebra.RingHom")
*** Failed to load theory "HOL-Algebra.More_Group" (unresolved "HOL-Algebra.Ring")
*** Failed to load theory "HOL-Algebra.More_Finite_Product" (unresolved "HOL-Algebra.More_Group")
*** Failed to load theory "HOL-Algebra.More_Ring" (unresolved "HOL-Algebra.Ring")
*** Failed to load theory "HOL-Algebra.IntRing" (unresolved "HOL-Algebra.Lattice", "HOL-Algebra.QuotRing")
*** Failed to load theory "HOL-Algebra.Multiplicative_Group" (unresolved "HOL-Algebra.Coset", "HOL-Algebra.Group", "HOL-Algebra.More_Finite_Product", "HOL-Algebra.More_Group", "HOL-Algebra.UnivPoly")
*** Failed to build document in "/media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Algebra/outline"
*** Type unification failed
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  le ::
***   ('a, ??'a) gorder_scheme
***   \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool
*** Operand:   L :: ('a, 'b) eq_object_scheme
*** 
*** At command "locale" (line 32 of "~~/src/HOL/Algebra/Order.thy")