Loading theory "HOL-Number_Theory.Cong" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
Loading theory "HOL-Algebra.Congruence" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.More_Group" via "HOL-Algebra.Ring" via "HOL-Algebra.FiniteProduct" via "HOL-Algebra.Group" via "HOL-Algebra.Complete_Lattice" via "HOL-Algebra.Lattice" via "HOL-Algebra.Order")
class unique_euclidean_semiring = euclidean_semiring_cancel +
  fixes division_segment :: "'a \<Rightarrow> 'a" 
  assumes
    "euclidean_size_mult":
      "\<And>a b.
          euclidean_size (a * b) = euclidean_size a * euclidean_size b"
  assumes
    "is_unit_division_segment": "\<And>a. is_unit (division_segment a)"
    and
    "division_segment_mult":
      "\<And>a b.
          \<lbrakk>a \<noteq> (0::'a); b \<noteq> (0::'a)\<rbrakk>
          \<Longrightarrow> division_segment (a * b) =
                            division_segment a * division_segment b"
    and
    "division_segment_mod":
      "\<And>b a.
          \<lbrakk>b \<noteq> (0::'a); \<not> b dvd a\<rbrakk>
          \<Longrightarrow> division_segment (a mod b) = division_segment b"
  assumes
    "div_bounded":
      "\<And>b r q.
          \<lbrakk>b \<noteq> (0::'a);
           division_segment r = division_segment b;
           euclidean_size r < euclidean_size b\<rbrakk>
          \<Longrightarrow> (q * b + r) div b = q"
locale equivalence
  fixes S :: "('a, 'b) eq_object_scheme"   (structure)
  assumes "equivalence S"
### theory "HOL-Algebra.Congruence"
### 1.119s elapsed time, 2.268s cpu time, 0.000s GC time
Loading theory "HOL-Algebra.Order" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.More_Group" via "HOL-Algebra.Ring" via "HOL-Algebra.FiniteProduct" via "HOL-Algebra.Group" via "HOL-Algebra.Complete_Lattice" via "HOL-Algebra.Lattice")
### theory "HOL-Number_Theory.Cong"
### 1.489s elapsed time, 2.976s cpu time, 0.196s GC time
Loading theory "HOL-Number_Theory.Eratosthenes" (required by "HOL-Number_Theory.Number_Theory")
### theory "HOL-Algebra.Order"
### 0.436s elapsed time, 0.840s cpu time, 0.196s GC time
Loading theory "HOL-Number_Theory.Fib" (required by "HOL-Number_Theory.Number_Theory")
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
### theory "HOL-Number_Theory.Eratosthenes"
### 0.299s elapsed time, 0.600s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Prime_Powers" (required by "HOL-Number_Theory.Number_Theory")
### theory "HOL-Number_Theory.Fib"
### 0.343s elapsed time, 0.688s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Totient" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
consts
  totient_naive ::
    "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
### theory "HOL-Number_Theory.Totient"
### 0.617s elapsed time, 1.236s cpu time, 0.000s GC time
### theory "HOL-Number_Theory.Prime_Powers"
### 0.891s elapsed time, 1.784s cpu time, 0.000s GC time
### Rule already declared as introduction (intro)
### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOL-Number_Theory/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.Group" (unresolved "HOL-Algebra.Complete_Lattice")
*** Failed to load theory "HOL-Algebra.Coset" (unresolved "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.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.Multiplicative_Group" (unresolved "HOL-Algebra.Coset", "HOL-Algebra.Group", "HOL-Algebra.More_Finite_Product", "HOL-Algebra.More_Group", "HOL-Algebra.UnivPoly")
*** Failed to load theory "HOL-Number_Theory.Residues" (unresolved "HOL-Algebra.More_Finite_Product", "HOL-Algebra.More_Group", "HOL-Algebra.More_Ring", "HOL-Algebra.Multiplicative_Group")
*** Failed to load theory "HOL-Number_Theory.Euler_Criterion" (unresolved "HOL-Number_Theory.Residues")
*** Failed to load theory "HOL-Number_Theory.Gauss" (unresolved "HOL-Number_Theory.Euler_Criterion")
*** Failed to load theory "HOL-Number_Theory.Quadratic_Reciprocity" (unresolved "HOL-Number_Theory.Gauss")
*** Failed to load theory "HOL-Number_Theory.Pocklington" (unresolved "HOL-Number_Theory.Residues")
*** Failed to load theory "HOL-Number_Theory.Number_Theory" (unresolved "HOL-Number_Theory.Pocklington", "HOL-Number_Theory.Quadratic_Reciprocity", "HOL-Number_Theory.Residues")
*** 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")