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.379s elapsed time, 2.284s 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")
locale
 
weak_partial_order


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_partial_order L"
locale
 
weak_partial_order


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_partial_order L"
### theory "HOL-Number_Theory.Cong"
### 1.969s elapsed time, 3.436s cpu time, 0.204s GC time
Loading theory "HOL-Number_Theory.Eratosthenes" (required by "HOL-Number_Theory.Number_Theory")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale
 
weak_partial_order


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_partial_order L"
### theory "HOL-Number_Theory.Eratosthenes"
### 0.314s elapsed time, 0.628s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Fib" (required by "HOL-Number_Theory.Number_Theory")
Found termination order: "size <*mlex*> {}"
locale
 
partial_order


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "partial_order L"
locale
 
weak_partial_order_bottom


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_partial_order_bottom L"
Found termination order: "(\<lambda>p. size (snd (snd p))) <*mlex*> {}"
locale
 
weak_partial_order_top


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_partial_order_top L"
locale
 
weak_total_order


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_total_order L"
### theory "HOL-Number_Theory.Fib"
### 0.330s elapsed time, 0.664s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Prime_Powers" (required by "HOL-Number_Theory.Number_Theory")
locale
 
total_order


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "total_order L"
### theory "HOL-Algebra.Order"
### 1.275s elapsed time, 2.516s cpu time, 0.204s GC time
Loading theory "HOL-Algebra.Lattice" (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")
locale
 
weak_upper_semilattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_upper_semilattice L"
locale
 
weak_lower_semilattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_lower_semilattice L"
locale
 
weak_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_lattice L"
### theory "HOL-Number_Theory.Prime_Powers"
### 0.617s elapsed time, 1.236s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Totient" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
locale
 
weak_bounded_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_bounded_lattice L"
locale
 
upper_semilattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "upper_semilattice L"
consts
  totient_naive ::
    "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
locale
 
lower_semilattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "lower_semilattice L"
locale
 
Lattice.lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "lattice L"
### theory "HOL-Number_Theory.Totient"
### 0.746s elapsed time, 1.484s cpu time, 0.000s GC time
Loading theory "Matrix.Utility" (required by "Polynomial_Factorization.Prime_Factorization" via "Polynomial_Factorization.Missing_List")
locale
 
Lattice.bounded_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "bounded_lattice L"
locale
 
Lattice.bounded_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "bounded_lattice L"
### theory "HOL-Algebra.Lattice"
### 1.582s elapsed time, 3.152s cpu time, 0.000s GC time
Loading theory "HOL-Algebra.Complete_Lattice" (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")
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
locale
 
weak_complete_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_complete_lattice L"
Found termination order: "size_list size <*mlex*> {}"
### theory "Matrix.Utility"
### 0.776s elapsed time, 1.492s cpu time, 0.656s GC time
Loading theory "Polynomial_Factorization.Missing_List" (required by "Polynomial_Factorization.Prime_Factorization")
locale
 
weak_complete_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_complete_lattice L"
Found termination order: "size_list length <*mlex*> {}"
locale
 
weak_complete_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_complete_lattice L"
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
locale
 
Complete_Lattice.complete_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "complete_lattice L"
Found termination order: "length <*mlex*> {}"
locale
 
Complete_Lattice.complete_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "complete_lattice L"
locale
 
weak_complete_lattice


fixes L :: "('a, 'b) gorder_scheme"   (structure)


assumes "weak_complete_lattice L"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "HOL-Algebra.Complete_Lattice"
### 1.460s elapsed time, 2.868s cpu time, 0.656s GC time
Loading theory "HOL-Algebra.Group" (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")
consts
  list_union :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
consts
  list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
### Ignoring duplicate rewrite rule:
### set ?xs1 \<subseteq> set ?ys1 \<equiv>
### list_all (\<lambda>x. x \<in> set ?ys1) ?xs1
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
overloading
  nat_pow \<equiv> pow ::
    ('a, 'b) monoid_scheme
    \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a
overloading
  int_pow \<equiv> pow ::
    ('a, 'b) monoid_scheme
    \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a
locale
 
Group.monoid


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.monoid G"
Found termination order:
  "(\<lambda>p. length (snd p)) <*mlex*>
   (\<lambda>p. length (fst p)) <*mlex*> {}"
### Missing patterns in function definition:
### min_list [] = undefined
locale
 
Group.group


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.group G"
Found termination order: "length <*mlex*> {}"
consts
  permut_aux ::
    "'a list
     \<Rightarrow> (nat \<Rightarrow> nat)
                   \<Rightarrow> 'a list \<Rightarrow> 'a list"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale
 
subgroup


fixes H :: "'a set" 
  and G :: "('a, 'b) monoid_scheme"   (structure)


assumes "subgroup H G"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale
 
group_hom


fixes G :: "('a, 'b) monoid_scheme"   (structure)
  and H :: "('c, 'd) monoid_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 


assumes "group_hom G H h"
locale
 
Group.comm_monoid


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.comm_monoid G"
locale
 
comm_group


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "comm_group G"
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
### theory "HOL-Algebra.Group"
### 1.914s elapsed time, 3.792s cpu time, 0.812s GC time
Loading theory "HOL-Algebra.Coset" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.Multiplicative_Group")
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale
 
normal


fixes H :: "'a set" 
  and G :: "('a, 'b) monoid_scheme"   (structure)


assumes "normal H G"
### theory "Polynomial_Factorization.Missing_List"
### 3.022s elapsed time, 6.012s cpu time, 0.812s GC time
Loading theory "HOL-Algebra.FiniteProduct" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.More_Group" via "HOL-Algebra.Ring")
Proofs for inductive predicate(s) "foldSetDp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
locale
 
LCD


fixes B :: "'b set" 
  and D :: "'a set" 
  and f :: "'b \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "\<cdot>" 70)


assumes "LCD B D op \<cdot>"
locale
 
ACeD


fixes D :: "'a set" 
  and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"   (infixl "\<cdot>" 70)
  and e :: "'a" 


assumes "ACeD D op \<cdot> e"
### Ambiguous input (line 596 of "~~/src/HOL/Algebra/Coset.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>r_congruent_indexed" ("_index" ("_position" G))
###     ("\<^const>HOL.eq" ("_position" H)
###       ("_Coll" ("_pattern" ("_position" x) ("_position" y))
###         ("\<^const>HOL.conj"
###           ("\<^const>Set.member" ("_position" x)
###             ("_applC" ("_position" carrier) ("_position" G)))
###           ("\<^const>HOL.conj"
###             ("\<^const>Set.member" ("_position" y)
###               ("_applC" ("_position" carrier) ("_position" G)))
###             ("\<^const>Set.member"
###               ("\<^const>Group.monoid.mult_indexed"
###                 ("\<^const>Group.m_inv_indexed" ("_index" ("_position" G))
###                   ("_position" x))
###                 ("_index" ("_position" G)) ("_position" y))
###               ("_position" H))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^fixed>r_congruent_indexed" ("_index" ("_position" G))
###       ("_position" H))
###     ("_Coll" ("_pattern" ("_position" x) ("_position" y))
###       ("\<^const>HOL.conj"
###         ("\<^const>Set.member" ("_position" x)
###           ("_applC" ("_position" carrier) ("_position" G)))
###         ("\<^const>HOL.conj"
###           ("\<^const>Set.member" ("_position" y)
###             ("_applC" ("_position" carrier) ("_position" G)))
###           ("\<^const>Set.member"
###             ("\<^const>Group.monoid.mult_indexed"
###               ("\<^const>Group.m_inv_indexed" ("_index" ("_position" G))
###                 ("_position" x))
###               ("_index" ("_position" G)) ("_position" y))
###             ("_position" H)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 648 of "~~/src/HOL/Algebra/Coset.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" a) ("_indexdefault")
###       ("_position" H))
###     ("\<^const>Coset.r_congruent_indexed" ("_indexdefault")
###       ("\<^const>Relation.Image" ("_position" H)
###         ("_Finset" ("_position" a))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" a) ("_indexdefault")
###       ("_position" H))
###     ("\<^const>Relation.Image"
###       ("\<^const>Coset.r_congruent_indexed" ("_indexdefault")
###         ("_position" H))
###       ("_Finset" ("_position" a)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
locale
 
Group.comm_monoid


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.comm_monoid G"
locale
 
Group.comm_monoid


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.comm_monoid G"
### theory "HOL-Algebra.FiniteProduct"
### 0.572s elapsed time, 1.152s cpu time, 0.000s GC time
Loading theory "HOL-Algebra.Ring" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.More_Group")
### theory "HOL-Algebra.Coset"
### 1.050s elapsed time, 2.112s cpu time, 0.000s GC time
Loading theory "Polynomial_Factorization.Missing_Multiset" (required by "Polynomial_Factorization.Prime_Factorization")
locale
 
abelian_monoid


fixes G :: "('a, 'b) ring_scheme"   (structure)


assumes "abelian_monoid G"
locale
 
abelian_group


fixes G :: "('a, 'b) ring_scheme"   (structure)


assumes "abelian_group G"
locale
 
abelian_monoid


fixes G :: "('a, 'b) ring_scheme"   (structure)


assumes "abelian_monoid G"
### theory "Polynomial_Factorization.Missing_Multiset"
### 0.226s elapsed time, 0.452s cpu time, 0.000s GC time
Loading theory "Polynomial_Factorization.Prime_Factorization"
locale
 
abelian_monoid


fixes G :: "('a, 'b) ring_scheme"   (structure)


assumes "abelian_monoid G"
locale
 
abelian_group


fixes G :: "('a, 'b) ring_scheme"   (structure)


assumes "abelian_group G"
locale
 
Ring.semiring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "semiring R"
locale
 
Ring.ring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "ring R"
### theory "Polynomial_Factorization.Prime_Factorization"
### 1.158s elapsed time, 2.292s cpu time, 0.600s GC time
locale
 
cring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "cring R"
locale
 
domain


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "domain R"
locale
 
Ring.field


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "field R"
locale
 
Ring.ring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "ring R"
locale
 
Ring.ring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "ring R"
### ML warning (line 45 of "~~/src/HOL/Algebra/ringsimp.ML"):
### Value identifier (s) has not been referenced.
### ML warning (line 48 of "~~/src/HOL/Algebra/ringsimp.ML"):
### Matches are not exhaustive.
signature RINGSIMP =
  sig
    val add_struct: string * term list -> attribute
    val algebra_tac: Proof.context -> int -> tactic
    val del_struct: string * term list -> attribute
    val print_structures: Proof.context -> unit
  end
structure Ringsimp: RINGSIMP
locale
 
Ring.semiring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "semiring R"
locale
 
domain


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "domain R"
locale
 
ring_hom_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and S :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 


assumes "ring_hom_cring R S h"
### theory "HOL-Algebra.Ring"
### 5.190s elapsed time, 10.332s cpu time, 0.756s GC time
Loading theory "HOL-Algebra.AbelCoset" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.Multiplicative_Group" via "HOL-Algebra.UnivPoly" via "HOL-Algebra.RingHom" via "HOL-Algebra.Ideal")
locale
 
abelian_group_hom


fixes G :: "('a, 'b) ring_scheme"   (structure)
  and H :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 


assumes "abelian_group_hom G H h"
locale
 
additive_subgroup


fixes H :: "'a set" 
  and G :: "('a, 'b) ring_scheme"   (structure)


assumes "additive_subgroup H G"
locale
 
abelian_subgroup


fixes H :: "'a set" 
  and G :: "('a, 'b) ring_scheme"   (structure)


assumes "abelian_subgroup H G"
Loading theory "HOL-Algebra.Module" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.Multiplicative_Group" via "HOL-Algebra.UnivPoly")
locale
 
module


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and M :: "('a, 'c, 'd) module_scheme"   (structure)


assumes "module R M"
locale
 
algebra


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and M :: "('a, 'c, 'd) module_scheme"   (structure)


assumes "algebra R M"
### theory "HOL-Algebra.Module"
### 2.818s elapsed time, 5.616s cpu time, 0.268s GC time
Loading theory "HOL-Algebra.More_Group" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
### theory "HOL-Algebra.More_Group"
### 0.143s elapsed time, 0.288s cpu time, 0.000s GC time
Loading theory "HOL-Algebra.More_Finite_Product" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
### theory "HOL-Algebra.More_Finite_Product"
### 0.489s elapsed time, 0.976s cpu time, 0.000s GC time
Loading theory "HOL-Algebra.More_Ring" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
### theory "HOL-Algebra.More_Ring"
### 0.554s elapsed time, 1.080s cpu time, 0.388s GC time
### theory "HOL-Algebra.AbelCoset"
### 7.943s elapsed time, 15.784s cpu time, 1.096s GC time
Loading theory "HOL-Algebra.Ideal" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.Multiplicative_Group" via "HOL-Algebra.UnivPoly" via "HOL-Algebra.RingHom")
locale
 
ideal


fixes I :: "'a set" 
  and R :: "('a, 'b) ring_scheme"   (structure)


assumes "ideal I R"
locale
 
principalideal


fixes I :: "'a set" 
  and R :: "('a, 'b) ring_scheme"   (structure)


assumes "principalideal I R"
locale
 
maximalideal


fixes I :: "'a set" 
  and R :: "('a, 'b) ring_scheme"   (structure)


assumes "maximalideal I R"
locale
 
primeideal


fixes I :: "'a set" 
  and R :: "('a, 'b) ring_scheme"   (structure)


assumes "primeideal I R"
### Rule already declared as introduction (intro)
### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
### theory "HOL-Algebra.Ideal"
### 5.679s elapsed time, 11.252s cpu time, 0.820s GC time
Loading theory "HOL-Algebra.RingHom" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.Multiplicative_Group" via "HOL-Algebra.UnivPoly")
locale
 
ring_hom_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and S :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 


assumes "ring_hom_ring R S h"
### theory "HOL-Algebra.RingHom"
### 2.215s elapsed time, 4.396s cpu time, 0.212s GC time
Loading theory "HOL-Algebra.UnivPoly" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues" via "HOL-Algebra.Multiplicative_Group")
locale
 
bound


fixes z :: "'a" 
  and n :: "nat" 
  and f :: "nat \<Rightarrow> 'a" 


assumes "bound z n f"
locale
 
Ring.ring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "ring R"
locale
 
UP


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_cring R"


defines "P \<equiv> UP R"
locale
 
UP_domain


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_domain R"


defines "P \<equiv> UP R"
locale
 
UP


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_cring R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_domain


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_domain R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_domain


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_domain R"


defines "P \<equiv> UP R"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_domain


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_domain R"


defines "P \<equiv> UP R"
locale
 
Ring.ring


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "ring R"
locale
 
UP


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


defines "P \<equiv> UP R"
locale
 
UP_pre_univ_prop


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and S :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_pre_univ_prop R S h"


defines "P \<equiv> UP R"
locale
 
UP_univ_prop


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and S :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)
  and s :: "'c" 
  and Eval :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'c" 


assumes "UP_univ_prop R S h s"


defines "P \<equiv> UP R"
  and "Eval \<equiv> eval R S h s"
locale
 
UP_pre_univ_prop


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and S :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_pre_univ_prop R S h"


defines "P \<equiv> UP R"
locale
 
UP_pre_univ_prop


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and S :: "('c, 'd) ring_scheme"   (structure)
  and h :: "'a \<Rightarrow> 'c" 
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_pre_univ_prop R S h"


defines "P \<equiv> UP R"
locale
 
Group.monoid


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.monoid G"
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_cring R"


defines "P \<equiv> UP R"
locale
 
UP_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_cring R"


defines "P \<equiv> UP R"
### theory "HOL-Algebra.UnivPoly"
### 24.825s elapsed time, 49.100s cpu time, 2.960s GC time
Loading theory "HOL-Algebra.Multiplicative_Group" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Residues")
locale
 
UP_ring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_ring R"


defines "P \<equiv> UP R"
locale
 
UP_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_cring R"


defines "P \<equiv> UP R"
locale
 
Group.group


fixes G :: "('a, 'b) monoid_scheme"   (structure)


assumes "Group.group G"
locale
 
Ring.field


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "field R"
locale
 
UP_cring


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_cring R"


defines "P \<equiv> UP R"
locale
 
UP_domain


fixes R :: "('a, 'b) ring_scheme"   (structure)
  and P :: "('a, nat \<Rightarrow> 'a) up_ring"   (structure)


assumes "UP_domain R"


defines "P \<equiv> UP R"
locale
 
Ring.field


fixes R :: "('a, 'b) ring_scheme"   (structure)


assumes "field R"
### theory "HOL-Algebra.Multiplicative_Group"
### 5.739s elapsed time, 11.420s cpu time, 0.420s GC time
Loading theory "HOL-Number_Theory.Residues" (required by "HOL-Number_Theory.Number_Theory")
locale
 
residues


fixes m :: "int" 
  and R :: "int ring"   (structure)


assumes "residues m"


defines "R \<equiv> residue_ring m"
locale
 
residues


fixes m :: "int" 
  and R :: "int ring"   (structure)


assumes "residues m"


defines "R \<equiv> residue_ring m"
locale
 
residues_prime


fixes p :: "nat" 
  and R :: "int ring"   (structure)


assumes "residues_prime p"


defines "R \<equiv> residue_ring (int p)"
locale
 
residues_prime


fixes p :: "nat" 
  and R :: "int ring"   (structure)


assumes "residues_prime p"


defines "R \<equiv> residue_ring (int p)"
### theory "HOL-Number_Theory.Residues"
### 4.088s elapsed time, 8.088s cpu time, 0.516s GC time
Loading theory "HOL-Number_Theory.Euler_Criterion" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Quadratic_Reciprocity" via "HOL-Number_Theory.Gauss")
### theory "HOL-Number_Theory.Euler_Criterion"
### 0.175s elapsed time, 0.352s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Gauss" (required by "HOL-Number_Theory.Number_Theory" via "HOL-Number_Theory.Quadratic_Reciprocity")
locale
 
GAUSS


fixes p :: "nat" 
  and a :: "int" 


assumes "GAUSS p a"
### theory "HOL-Number_Theory.Gauss"
### 0.289s elapsed time, 0.580s cpu time, 0.000s GC time
Loading theory "HOL-Number_Theory.Quadratic_Reciprocity" (required by "HOL-Number_Theory.Number_Theory")
locale
 
QR


fixes p :: "nat" 
  and q :: "nat" 


assumes "QR p q"
Loading theory "HOL-Number_Theory.Pocklington" (required by "HOL-Number_Theory.Number_Theory")
### theory "HOL-Number_Theory.Pocklington"
### 0.304s elapsed time, 0.612s cpu time, 0.000s GC time
### theory "HOL-Number_Theory.Quadratic_Reciprocity"
### 0.579s elapsed time, 1.132s cpu time, 0.168s GC time
Loading theory "HOL-Number_Theory.Number_Theory"
### theory "HOL-Number_Theory.Number_Theory"
### 1.288s elapsed time, 2.572s 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
### Rule already declared as introduction (intro)
### \<lbrakk>?P ?x; ?x \<in> ?A\<rbrakk>
### \<Longrightarrow> \<exists>x\<in>?A. ?P x
### Rule already declared as introduction (intro)
### \<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<oplus> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<zero> \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow>
### \<ominus> ?x1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<ominus> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<otimes> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<one> \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<zero> \<oplus> ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<one> \<otimes> ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> ?y \<oplus> \<zero> \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<ominus> (\<ominus> ?y) \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<ominus> \<zero> \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow> \<zero> \<otimes> ?x1 \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow> ?x1 \<otimes> \<zero> \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<oplus> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<zero> \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow>
### \<ominus> ?x1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<ominus> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<otimes> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<one> \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<zero> \<oplus> ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<one> \<otimes> ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> ?y \<oplus> \<zero> \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<ominus> (\<ominus> ?y) \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<ominus> \<zero> \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow> \<zero> \<otimes> ?x1 \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow> ?x1 \<otimes> \<zero> \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<oplus> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<zero> \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow>
### \<ominus> ?x1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<ominus> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<lbrakk>?x1 \<in> carrier R; ?y1 \<in> carrier R\<rbrakk>
### \<Longrightarrow> ?x1 \<otimes> ?y1 \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### \<one> \<in> carrier R \<equiv> True
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<zero> \<oplus> ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<one> \<otimes> ?y \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> ?y \<oplus> \<zero> \<equiv> ?y
### Ignoring duplicate rewrite rule:
### ?y \<in> carrier R \<Longrightarrow> \<ominus> (\<ominus> ?y) \<equiv> ?y
### Ignoring duplicate rewrite rule:
### \<ominus> \<zero> \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow> \<zero> \<otimes> ?x1 \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?x1 \<in> carrier R \<Longrightarrow> ?x1 \<otimes> \<zero> \<equiv> \<zero>
### Ignoring duplicate rewrite rule:
### ?a1 dvd ?y \<Longrightarrow> ?a1 * (?y div ?a1) \<equiv> ?y
### Legacy feature! Old 'def' command -- use 'define' instead
### Ignoring duplicate rewrite rule:
### ?a1 dvd ?y \<Longrightarrow> ?a1 * (?y div ?a1) \<equiv> ?y
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
(\<lambda>n. mset (prime_factorization_nat n)) = prime_factorization
Loading theory "Dirichlet_Series.Dirichlet_Misc" (required by "Dirichlet_Series.Arithmetic_Summatory_Asymptotics" via "Dirichlet_Series.Arithmetic_Summatory" via "Dirichlet_Series.More_Totient" via "Dirichlet_Series.Moebius_Mu" via "Dirichlet_Series.Dirichlet_Series" via "Dirichlet_Series.Dirichlet_Product" via "Dirichlet_Series.Multiplicative_Function")
### theory "Dirichlet_Series.Dirichlet_Misc"
### 0.265s elapsed time, 0.564s cpu time, 0.000s GC time
isabelle document -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_Series/document 2>&1
isabelle document -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Dirichlet_Series/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) (./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) (./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)

LaTeX Warning: Citation `apostol' on page 1 undefined on input line 20.

(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (1.31284pt too wide) in paragraph at lines 22--23
[]\OT1/cmr/m/n/10 Definitions and ba-sic prop-er-ties for sev-eral number-theor
etic func-
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2] (./session.tex
(./Dirichlet_Misc.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'.


LaTeX Warning: There were undefined references.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
>
Output written on root.pdf (2 pages, 81829 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
Database file #1: root.bib
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) (./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) (./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))
(./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))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)

LaTeX Warning: Citation `apostol' on page 1 undefined on input line 20.

(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (1.31284pt too wide) in paragraph at lines 22--23
[]\OT1/cmr/m/n/10 Definitions and ba-sic prop-er-ties for sev-eral number-theor
etic func-
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] (./root.toc) [2]
(./session.tex (./Dirichlet_Misc.tex)) (./root.bbl) [3] (./root.aux)

LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
>
Output written on root.pdf (3 pages, 87920 bytes).
Transcript written on root.log.
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) (./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) (./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))
(./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))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (1.31284pt too wide) in paragraph at lines 22--23
[]\OT1/cmr/m/n/10 Definitions and ba-sic prop-er-ties for sev-eral number-theor
etic func-
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] (./root.toc) [2]
(./session.tex (./Dirichlet_Misc.tex)) (./root.bbl) [3] (./root.aux) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
>
Output written on root.pdf (3 pages, 87601 bytes).
Transcript written on root.log.

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) (./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)

LaTeX Warning: Citation `apostol' on page 1 undefined on input line 20.

(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (1.31284pt too wide) in paragraph at lines 22--23
[]\OT1/cmr/m/n/10 Definitions and ba-sic prop-er-ties for sev-eral number-theor
etic func-
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2] (./session.tex
(./Dirichlet_Misc.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'.


LaTeX Warning: There were undefined references.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
>
Output written on root.pdf (2 pages, 81829 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
Database file #1: root.bib
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) (./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))
(./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))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)

LaTeX Warning: Citation `apostol' on page 1 undefined on input line 20.

(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (1.31284pt too wide) in paragraph at lines 22--23
[]\OT1/cmr/m/n/10 Definitions and ba-sic prop-er-ties for sev-eral number-theor
etic func-
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] (./root.toc) [2]
(./session.tex (./Dirichlet_Misc.tex)) (./root.bbl) [3] (./root.aux)

LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
>
Output written on root.pdf (3 pages, 87920 bytes).
Transcript written on root.log.
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) (./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))
(./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))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd)
Overfull \hbox (1.31284pt too wide) in paragraph at lines 22--23
[]\OT1/cmr/m/n/10 Definitions and ba-sic prop-er-ties for sev-eral number-theor
etic func-
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] (./root.toc) [2]
(./session.tex (./Dirichlet_Misc.tex)) (./root.bbl) [3] (./root.aux) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
>
Output written on root.pdf (3 pages, 87601 bytes).
Transcript written on root.log.

*** Failed to load theory "Dirichlet_Series.Multiplicative_Function" (unresolved "Dirichlet_Series.Dirichlet_Misc")
*** Failed to load theory "Dirichlet_Series.Dirichlet_Product" (unresolved "Dirichlet_Series.Multiplicative_Function")
*** Failed to load theory "Dirichlet_Series.Euler_Products" (unresolved "Dirichlet_Series.Multiplicative_Function")
*** Failed to load theory "Dirichlet_Series.Dirichlet_Series" (unresolved "Dirichlet_Series.Dirichlet_Product", "Dirichlet_Series.Multiplicative_Function")
*** Failed to load theory "Dirichlet_Series.Moebius_Mu" (unresolved "Dirichlet_Series.Dirichlet_Misc", "Dirichlet_Series.Dirichlet_Series")
*** Failed to load theory "Dirichlet_Series.More_Totient" (unresolved "Dirichlet_Series.Moebius_Mu")
*** Failed to load theory "Dirichlet_Series.Liouville_Lambda" (unresolved "Dirichlet_Series.Dirichlet_Series", "Dirichlet_Series.Moebius_Mu", "Dirichlet_Series.Multiplicative_Function")
*** Failed to load theory "Dirichlet_Series.Divisor_Count" (unresolved "Dirichlet_Series.Dirichlet_Series", "Dirichlet_Series.More_Totient")
*** Failed to load theory "Dirichlet_Series.Arithmetic_Summatory" (unresolved "Dirichlet_Series.Dirichlet_Series", "Dirichlet_Series.Divisor_Count", "Dirichlet_Series.Liouville_Lambda", "Dirichlet_Series.Moebius_Mu", "Dirichlet_Series.More_Totient")
*** Failed to load theory "Dirichlet_Series.Dirichlet_Efficient_Code" (unresolved "Dirichlet_Series.Divisor_Count", "Dirichlet_Series.Liouville_Lambda", "Dirichlet_Series.Moebius_Mu", "Dirichlet_Series.More_Totient")
*** Failed to load theory "Dirichlet_Series.Partial_Summation" (unresolved "Dirichlet_Series.Arithmetic_Summatory")
*** Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Dirichlet_Series", "Dirichlet_Series.Euler_Products", "Dirichlet_Series.Moebius_Mu", "Dirichlet_Series.Partial_Summation")
*** Failed to load theory "Dirichlet_Series.Arithmetic_Summatory_Asymptotics" (unresolved "Dirichlet_Series.Arithmetic_Summatory", "Dirichlet_Series.Dirichlet_Series_Analysis")
*** Undeclared class: "??.semiring_div" (line 143 of "~~/afp/thys/Dirichlet_Series/Dirichlet_Misc.thy")
*** At command "lemma" (line 141 of "~~/afp/thys/Dirichlet_Series/Dirichlet_Misc.thy")