Presenting theory "HOL-Algebra.Weak_Morphisms"
13:20:34Presenting theory "Constructive_Cryptography.Distinguisher"
13:20:35Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:20:35Presenting theory "VectorSpace.VectorSpace"
13:20:35Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
13:20:35Presenting theory "Executable_Randomized_Algorithms.Randomized_Algorithm"
13:20:35Presenting theory "HOL-Algebra.Ideal_Product"
13:20:36Presenting theory "Constructive_Cryptography.Wiring"
13:20:36Presenting theory "Jordan_Normal_Form.Spectral_Radius"
13:20:37Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:20:37Presenting theory "Perron_Frobenius.Bij_Nat"
13:20:37Presenting theory "Polynomial_Factorization.Polynomial_Irreducibility"
13:20:38Presenting theory "Polynomial_Factorization.Order_Polynomial"
13:20:38Presenting theory "HOL-Algebra.Chinese_Remainder"
13:20:38Presenting theory "Monomorphic_Monad.Monomorphic_Monad"
13:20:38Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:20:38Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
13:20:38Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:20:38Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:20:38Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:20:38Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:20:38Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:20:38Presenting theory "HOL-Algebra.Bij"
13:20:38Presenting theory "Perron_Frobenius.Cancel_Card_Constraint"
13:20:38Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML"
13:20:38Presenting theory "Finite_Fields.Find_Irreducible_Poly"
13:20:39Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:20:39Presenting theory "Universal_Hash_Families.Carter_Wegman_Hash_Family"
13:20:40Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:20:40Presenting theory "Jordan_Normal_Form.Missing_VectorSpace"
13:20:41Presenting theory "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families"
13:20:43Presenting theory "HOL-Eisbach.Eisbach"
13:20:43Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
13:20:43Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
13:20:43Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
13:20:43Presenting file "~~/src/HOL/Eisbach/match_method.ML"
13:20:43Presenting theory "HOL-Algebra.Group_Action"
13:20:43Presenting theory "Constructive_Cryptography.Constructive_Cryptography"
13:20:43Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
13:20:44Presenting theory "Perron_Frobenius.HMA_Connect"
13:20:44Presenting theory "Constructive_Cryptography.System_Construction"
13:20:44Presenting theory "MDP-Algorithms.Blinfun_To_Matrix"
13:20:45Presenting theory "Jordan_Normal_Form.Column_Operations"
13:20:45Presenting theory "MDP-Algorithms.Policy_Iteration_Fin"
13:20:45Presenting theory "Containers.Containers_Auxiliary"
13:20:45Presenting theory "HOL-Algebra.Zassenhaus"
13:20:46Presenting theory "Constructive_Cryptography.One_Time_Pad"
13:20:46Presenting theory "Polynomial_Factorization.Square_Free_Factorization"
13:20:46Presenting theory "Deriving.Generator_Aux"
13:20:46Presenting file "$AFP/Deriving/bnf_access.ML"
13:20:46Presenting file "$AFP/Deriving/generator_aux.ML"
13:20:47Presenting theory "Deriving.Derive_Manager"
13:20:47Presenting file "$AFP/Deriving/derive_manager.ML"
13:20:47Presenting theory "Containers.Containers_Auxiliary"
13:20:47Presenting theory "HOL-Algebra.Galois_Connection"
13:20:47Presenting theory "Containers.Containers_Generator"
13:20:47Presenting file "$AFP/Containers/containers_generator.ML"
13:20:48Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm"
13:20:48Presenting theory "Concentration_Inequalities.Bienaymes_Identity"
13:20:48Presenting theory "HOL-Algebra.Subrings"
13:20:49Presenting theory "Jordan_Normal_Form.VS_Connect"
13:20:49Presenting theory "HOL-Algebra.Generated_Rings"
13:20:49Presenting theory "Containers.Collection_Enum"
13:20:49Presenting file "$AFP/Containers/cenum_generator.ML"
13:20:50Presenting theory "HOL-Algebra.Generated_Fields"
13:20:50Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff"
13:20:50Presenting theory "Polynomial_Factorization.Missing_List"
13:20:51Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level"
13:20:51Presenting theory "Polynomial_Factorization.Missing_Multiset"
13:20:51Presenting theory "Deriving.Equality_Generator"
13:20:51Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
13:20:51Presenting theory "Deriving.Equality_Instances"
13:20:51Presenting theory "Berlekamp_Zassenhaus.More_Missing_Multiset"
13:20:51Presenting theory "HOL-Algebra.Product_Groups"
13:20:51Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy"
13:20:52Presenting theory "HOL-Cardinals.Fun_More"
13:20:52Presenting theory "Containers.Collection_Eq"
13:20:52Presenting file "$AFP/Containers/ceq_generator.ML"
13:20:52Presenting theory "Containers.Equal"
13:20:52Presenting theory "HOL-Combinatorics.List_Permutation"
13:20:52Presenting theory "Applicative_Lifting.Applicative"
13:20:52Presenting file "$AFP/Applicative_Lifting/applicative.ML"
13:20:52Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm"
13:20:53Presenting Constructive_Cryptography_CM in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography_CM" ...
13:20:53Presenting document Constructive_Cryptography_CM/document
13:20:53Presenting document Constructive_Cryptography_CM/outline
13:20:53Presenting theory "HOL-Cardinals.Order_Relation_More"
13:20:53Presenting theory "Jordan_Normal_Form.Determinant"
13:20:53Presenting theory "HOL-Cardinals.Wellfounded_More"
13:20:53Presenting theory "Sigma_Commit_Crypto.Xor"
13:20:53Presenting theory "Containers.DList_Set"
13:20:53Presenting theory "HOL-Cardinals.Wellorder_Relation"
13:20:54Presenting theory "HOL-Cardinals.Wellorder_Embedding"
13:20:54Presenting theory "HOL-Cardinals.Order_Union"
13:20:55Presenting theory "Containers.List_Fusion"
13:20:55Presenting theory "HOL-Library.Char_ord"
13:20:55Presenting theory "Containers.Lexicographic_Order"
13:20:56Presenting theory "Jordan_Normal_Form.Char_Poly"
13:20:56Presenting theory "Containers.Extend_Partial_Order"
13:20:56Presenting theory "HOL-Cardinals.Wellorder_Constructions"
13:20:56Presenting theory "Jordan_Normal_Form.Matrix_Kernel"
13:20:57Presenting theory "Constructive_Cryptography_CM.More_CC"
13:20:58Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form"
13:20:58Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness"
13:20:58Presenting theory "Containers.Set_Linorder"
13:20:59Presenting theory "VectorSpace.RingModuleFacts"
13:20:59Presenting theory "VectorSpace.FunctionLemmas"
13:20:59Presenting theory "Constructive_Cryptography.Message_Authentication_Code"
13:20:59Presenting theory "Deriving.Comparator"
13:20:59Presenting theory "VectorSpace.MonoidSums"
13:21:00Presenting theory "Constructive_Cryptography_CM.Observe_Failure"
13:21:00Presenting theory "Constructive_Cryptography.Secure_Channel"
13:21:00Presenting theory "Constructive_Cryptography.Examples"
13:21:00Presenting Game_Based_Crypto in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto" ...
13:21:00Presenting document Game_Based_Crypto/document
13:21:00Presenting document Game_Based_Crypto/outline
13:21:00Presenting theory "Constructive_Cryptography_CM.Fold_Spmf"
13:21:00Presenting theory "Game_Based_Crypto.Diffie_Hellman"
13:21:00Presenting theory "Jordan_Normal_Form.Gram_Schmidt"
13:21:00Presenting theory "HOL-Algebra.Divisibility"
13:21:01Presenting theory "Deriving.Comparator_Generator"
13:21:01Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
13:21:01Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
13:21:01Presenting theory "Deriving.Compare"
13:21:01Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
13:21:01Presenting theory "Deriving.Compare_Generator"
13:21:01Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
13:21:01Presenting theory "Deriving.Compare_Instances"
13:21:02Presenting theory "Containers.Collection_Order"
13:21:02Presenting file "$AFP/Containers/ccompare_generator.ML"
13:21:02Presenting theory "Game_Based_Crypto.IND_CCA2"
13:21:02Presenting theory "Game_Based_Crypto.IND_CCA2_sym"
13:21:03Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
13:21:03Presenting theory "VectorSpace.LinearCombinations"
13:21:03Presenting theory "Game_Based_Crypto.IND_CPA"
13:21:03Presenting theory "CryptHOL.Misc_CryptHOL"
13:21:03Presenting theory "Berlekamp_Zassenhaus.Unique_Factorization"
13:21:03Presenting theory "Game_Based_Crypto.IND_CPA_PK"
13:21:04Presenting theory "Applicative_Lifting.Applicative_PMF"
13:21:04Presenting theory "Jordan_Normal_Form.Schur_Decomposition"
13:21:04Presenting theory "Applicative_Lifting.Applicative_Set"
13:21:04Presenting theory "VectorSpace.SumSpaces"
13:21:04Presenting theory "HOL-Library.Groups_Big_Fun"
13:21:04Presenting theory "CryptHOL.Set_Applicative"
13:21:04Presenting theory "Game_Based_Crypto.IND_CPA_PK_Single"
13:21:04Presenting theory "CryptHOL.SPMF_Applicative"
13:21:04Presenting theory "HOL-Library.Fun_Lexorder"
13:21:04Presenting theory "CryptHOL.List_Bits"
13:21:04Presenting theory "Applicative_Lifting.Applicative_Environment"
13:21:04Presenting theory "CryptHOL.Environment_Functor"
13:21:04Presenting theory "Polynomial_Factorization.Missing_Polynomial_Factorial"
13:21:05Presenting theory "HOL-Library.More_List"
13:21:05Presenting theory "Game_Based_Crypto.SUF_CMA"
13:21:05Presenting theory "Jordan_Normal_Form.Missing_Misc"
13:21:05Presenting theory "Game_Based_Crypto.Pseudo_Random_Function"
13:21:05Presenting theory "Game_Based_Crypto.Pseudo_Random_Permutation"
13:21:06Presenting theory "CryptHOL.Partial_Function_Set"
13:21:06Presenting theory "VectorSpace.VectorSpace"
13:21:06Presenting theory "HOL-Library.Function_Algebras"
13:21:07Presenting theory "HOL-Algebra.FiniteProduct"
13:21:07Presenting theory "Landau_Symbols.Group_Sort"
13:21:07Presenting theory "HOL-Library.Poly_Mapping"
13:21:07Presenting theory "Game_Based_Crypto.Guessing_Many_One"
13:21:08Presenting theory "Game_Based_Crypto.Unpredictable_Function"
13:21:08Presenting theory "Game_Based_Crypto.Security_Spec"
13:21:08Presenting theory "Game_Based_Crypto.Elgamal"
13:21:09Presenting theory "Landau_Symbols.Landau_Real_Products"
13:21:09Presenting theory "HOL-Library.RBT_Impl"
13:21:10Presenting theory "Landau_Symbols.Landau_Simprocs"
13:21:10Presenting file "$AFP/Landau_Symbols/landau_simprocs.ML"
13:21:10Presenting theory "Jordan_Normal_Form.Missing_VectorSpace"
13:21:10Presenting theory "Landau_Symbols.Landau_More"
13:21:10Presenting theory "Containers.RBT_ext"
13:21:10Presenting theory "CryptHOL.Negligible"
13:21:10Presenting theory "Constructive_Cryptography_CM.Fused_Resource"
13:21:11Presenting theory "HOL-Algebra.Ring"
13:21:11Presenting theory "HOL-Algebra.Free_Abelian_Groups"
13:21:11Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:21:11Presenting theory "Game_Based_Crypto.Hashed_Elgamal"
13:21:11Presenting theory "Constructive_Cryptography_CM.State_Isomorphism"
13:21:11Presenting theory "HOL-Combinatorics.List_Permutation"
13:21:11Presenting theory "Deriving.RBT_Comparator_Impl"
13:21:11Presenting theory "Game_Based_Crypto.RP_RF"
13:21:12Presenting theory "Containers.RBT_Mapping2"
13:21:12Presenting theory "CryptHOL.Resumption"
13:21:12Presenting theory "Jordan_Normal_Form.Missing_Ring"
13:21:12Presenting theory "Game_Based_Crypto.PRF_UHF"
13:21:12Presenting theory "Jordan_Normal_Form.Conjugate"
13:21:12Presenting theory "Containers.RBT_Set2"
13:21:12Presenting theory "Containers.Closure_Set"
13:21:12Presenting theory "CryptHOL.Generat"
13:21:13Presenting theory "HOL-Algebra.Module"
13:21:13Presenting theory "Constructive_Cryptography_CM.Construction_Utility"
13:21:15Presenting theory "Jordan_Normal_Form.VS_Connect"
13:21:15Presenting theory "Game_Based_Crypto.PRF_IND_CPA"
13:21:15Presenting theory "Constructive_Cryptography_CM.Concrete_Security"
13:21:16Presenting theory "Jordan_Normal_Form.Gram_Schmidt"
13:21:17Presenting theory "Constructive_Cryptography_CM.Asymptotic_Security"
13:21:17Presenting theory "Constructive_Cryptography_CM.Key"
13:21:18Presenting theory "Constructive_Cryptography_CM.Channel"
13:21:18Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
13:21:18Presenting theory "Jordan_Normal_Form.Schur_Decomposition"
13:21:19Presenting theory "HOL-Algebra.Divisibility"
13:21:20Presenting theory "Jordan_Normal_Form.Spectral_Radius"
13:21:20Presenting theory "Perron_Frobenius.Bij_Nat"
13:21:22Presenting theory "Containers.Set_Impl"
13:21:22Presenting theory "HOL-Algebra.Embedded_Algebras"
13:21:22Presenting file "$AFP/Containers/set_impl_generator.ML"
13:21:22Presenting theory "Constructive_Cryptography_CM.One_Time_Pad"
13:21:22Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:21:22Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:21:22Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:21:22Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:21:22Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:21:22Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:21:22Presenting theory "Game_Based_Crypto.Diffie_Hellman"
13:21:23Presenting theory "HOL-Algebra.IntRing"
13:21:23Presenting theory "Jordan_Normal_Form.Matrix_IArray_Impl"
13:21:23Presenting theory "Perron_Frobenius.Cancel_Card_Constraint"
13:21:23Presenting theory "Jordan_Normal_Form.Matrix"
13:21:23Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML"
13:21:24Presenting theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl"
13:21:24Presenting theory "Game_Based_Crypto.PRF_UPF_IND_CCA"
13:21:24Presenting theory "CryptHOL.Generative_Probabilistic_Value"
13:21:24Presenting theory "Game_Based_Crypto.Cryptographic_Constructions"
13:21:24Presenting theory "Game_Based_Crypto.Game_Based_Crypto"
13:21:24Presenting theory "HOL-Library.LaTeXsugar"
13:21:24Presenting theory "HOL-Combinatorics.Cycles"
13:21:25Presenting theory "HOL-Algebra.Solvable_Groups"
13:21:26Presenting theory "Jordan_Normal_Form.Determinant_Impl"
13:21:26Presenting theory "HOL-Algebra.Sym_Groups"
13:21:27Presenting theory "HOL-Algebra.Exact_Sequence"
13:21:28Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
13:21:28Presenting theory "Show.Show"
13:21:28Presenting file "$AFP/Show/show_generator.ML"
13:21:29Presenting theory "Jordan_Normal_Form.Show_Matrix"
13:21:29Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
13:21:29Presenting theory "CryptHOL.Computational_Model"
13:21:29Presenting theory "Jordan_Normal_Form.Column_Operations"
13:21:29Presenting theory "Show.Show_Instances"
13:21:29Presenting theory "HOL-Algebra.Ring_Divisibility"
13:21:30Presenting theory "Show.Shows_Literal"
13:21:30Presenting theory "Jordan_Normal_Form.Shows_Literal_Matrix"
13:21:30Presenting theory "Jordan_Normal_Form.Spectral_Radius"
13:21:30Presenting theory "Jordan_Normal_Form.Matrix_Impl"
13:21:31Presenting theory "Perron_Frobenius.Bij_Nat"
13:21:31Presenting theory "Constructive_Cryptography_CM.Diffie_Hellman_CC"
13:21:31Presenting theory "Perron_Frobenius.Cancel_Card_Constraint"
13:21:31Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML"
13:21:32Presenting theory "Constructive_Cryptography_CM.DH_OTP"
13:21:32Presenting Multi_Party_Computation in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation" ...
13:21:32Presenting document Multi_Party_Computation/document
13:21:32Presenting document Multi_Party_Computation/outline
13:21:32Presenting theory "CryptHOL.GPV_Expectation"
13:21:32Presenting theory "HOL-Number_Theory.Cong"
13:21:32Presenting theory "Game_Based_Crypto.CryptHOL_Tutorial"
13:21:32Presenting theory "Multi_Party_Computation.Cyclic_Group_Ext"
13:21:32Presenting Sigma_Commit_Crypto in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto" ...
13:21:32Presenting document Sigma_Commit_Crypto/document
13:21:32Presenting document Sigma_Commit_Crypto/outline
13:21:33Presenting theory "MDP-Algorithms.PI_Code"
13:21:33Presenting theory "MDP-Algorithms.PI_Code_Export_Float"
13:21:33Presenting theory "MDP-Algorithms.PI_Code_Export_Rat"
13:21:33Presenting theory "HOL-Algebra.FiniteProduct"
13:21:33Presenting theory "Perron_Frobenius.HMA_Connect"
13:21:34Presenting theory "Isabelle_Marries_Dirac.Basics"
13:21:34Presenting theory "Sigma_Commit_Crypto.Commitment_Schemes"
13:21:34Presenting theory "CryptHOL.GPV_Bisim"
13:21:34Presenting theory "CryptHOL.GPV_Applicative"
13:21:34Presenting theory "Isabelle_Marries_Dirac.Binary_Nat"
13:21:34Presenting theory "HOL-Algebra.Congruence"
13:21:35Presenting theory "HOL-Algebra.Ring"
13:21:35Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:21:35Presenting theory "HOL-Algebra.Order"
13:21:35Presenting theory "HOL-Algebra.Module"
13:21:35Presenting theory "HOL-Number_Theory.Cong"
13:21:35Presenting theory "HOL-Eisbach.Eisbach"
13:21:35Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
13:21:35Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
13:21:35Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
13:21:35Presenting file "~~/src/HOL/Eisbach/match_method.ML"
13:21:35Presenting theory "HOL-Algebra.AbelCoset"
13:21:36Presenting theory "HOL-Algebra.Lattice"
13:21:36Presenting theory "Sigma_Commit_Crypto.Cyclic_Group_Ext"
13:21:36Presenting theory "HOL-Algebra.Ideal"
13:21:36Presenting theory "Sigma_Commit_Crypto.Discrete_Log"
13:21:36Presenting theory "HOL-Algebra.RingHom"
13:21:38Presenting theory "MDP-Algorithms.Backward_Induction"
13:21:38Presenting theory "HOL-Algebra.FiniteProduct"
13:21:38Presenting theory "HOL-Algebra.Complete_Lattice"
13:21:38Presenting theory "HOL-Algebra.Polynomials"
13:21:38Presenting theory "MDP-Algorithms.Fin_Code"
13:21:38Presenting theory "MDP-Algorithms.Fin_Code_Export_Float"
13:21:38Presenting theory "MDP-Algorithms.Fin_Code_Export_Rat"
13:21:38Presenting Projective_Measurements in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Projective_Measurements" ...
13:21:38Presenting document Projective_Measurements/document
13:21:38Presenting document Projective_Measurements/outline
13:21:39Presenting theory "Jordan_Normal_Form.Determinant"
13:21:39Presenting theory "Isabelle_Marries_Dirac.Quantum"
13:21:39Presenting theory "HOL-Algebra.UnivPoly"
13:21:39Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:21:39Presenting theory "Subresultants.More_Homomorphisms"
13:21:39Presenting theory "Perron_Frobenius.HMA_Connect"
13:21:39Presenting theory "HOL-Computational_Algebra.Field_as_Ring"
13:21:39Presenting theory "Jordan_Normal_Form.Missing_Misc"
13:21:40Presenting theory "HOL-Algebra.Generated_Groups"
13:21:40Presenting theory "HOL-Algebra.Congruence"
13:21:40Presenting theory "Isabelle_Marries_Dirac.Complex_Vectors"
13:21:40Presenting theory "HOL-Algebra.Elementary_Groups"
13:21:41Presenting theory "HOL-Algebra.Order"
13:21:41Presenting theory "Matrix.Utility"
13:21:41Presenting theory "HOL-Algebra.Multiplicative_Group"
13:21:41Presenting theory "Perron_Frobenius.Perron_Frobenius_Aux"
13:21:41Presenting theory "HOL-Algebra.Lattice"
13:21:42Presenting theory "Berlekamp_Zassenhaus.Unique_Factorization_Poly"
13:21:42Presenting theory "HOL-Algebra.Ring"
13:21:42Presenting theory "HOL-Number_Theory.Totient"
13:21:42Presenting theory "Regular-Sets.Regular_Set"
13:21:42Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:21:42Presenting theory "HOL-Number_Theory.Residues"
13:21:42Presenting theory "Multi_Party_Computation.Number_Theory_Aux"
13:21:43Presenting theory "Multi_Party_Computation.Uniform_Sampling"
13:21:43Presenting theory "Perron_Frobenius.Perron_Frobenius"
13:21:43Presenting theory "Regular-Sets.Regular_Exp"
13:21:43Presenting theory "Multi_Party_Computation.Semi_Honest_Def"
13:21:43Presenting theory "HOL-Algebra.Complete_Lattice"
13:21:43Presenting theory "Multi_Party_Computation.OT_Functionalities"
13:21:43Presenting theory "Multi_Party_Computation.ETP"
13:21:43Presenting theory "Regular-Sets.NDerivative"
13:21:43Presenting theory "HOL-Algebra.Module"
13:21:43Presenting theory "Multi_Party_Computation.ETP_OT"
13:21:44Presenting theory "Multi_Party_Computation.ETP_RSA_OT"
13:21:44Presenting theory "Multi_Party_Computation.Noar_Pinkas_OT"
13:21:45Presenting theory "HOL-Library.While_Combinator"
13:21:45Presenting theory "Perron_Frobenius.Roots_Unity"
13:21:45Presenting theory "HOL-Algebra.Group"
13:21:45Presenting theory "Rank_Nullity_Theorem.Dual_Order"
13:21:45Presenting theory "HOL-Algebra.AbelCoset"
13:21:45Presenting theory "Berlekamp_Zassenhaus.Poly_Mod"
13:21:45Presenting theory "HOL-Algebra.Group"
13:21:46Presenting theory "Regular-Sets.Equivalence_Checking"
13:21:46Presenting theory "HOL-Algebra.Polynomial_Divisibility"
13:21:46Presenting theory "Multi_Party_Computation.OT14"
13:21:46Presenting theory "Regular-Sets.Relation_Interpretation"
13:21:46Presenting theory "Regular-Sets.Regexp_Method"
13:21:46Presenting theory "Rank_Nullity_Theorem.Mod_Type"
13:21:47Presenting theory "Multi_Party_Computation.GMW"
13:21:47Presenting theory "HOL-Library.Function_Algebras"
13:21:47Presenting theory "HOL-Algebra.Ideal"
13:21:47Presenting theory "Abstract-Rewriting.Seq"
13:21:47Presenting theory "HOL-Number_Theory.Cong"
13:21:47Presenting theory "HOL-Algebra.RingHom"
13:21:47Presenting theory "Multi_Party_Computation.Secure_Multiplication"
13:21:48Presenting theory "HOL-Algebra.FiniteProduct"
13:21:48Presenting theory "Multi_Party_Computation.DH_Ext"
13:21:48Presenting theory "Multi_Party_Computation.Malicious_Defs"
13:21:48Presenting theory "Rank_Nullity_Theorem.Miscellaneous"
13:21:49Presenting theory "HOL-Algebra.AbelCoset"
13:21:49Presenting theory "HOL-Algebra.Indexed_Polynomials"
13:21:49Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
13:21:50Presenting theory "Abstract-Rewriting.SN_Orders"
13:21:50Presenting theory "Matrix.Ordered_Semiring"
13:21:50Presenting theory "HOL-Algebra.Coset"
13:21:51Presenting theory "CryptHOL.Cyclic_Group"
13:21:51Presenting theory "CryptHOL.Cyclic_Group_SPMF"
13:21:51Presenting theory "CryptHOL.CryptHOL"
13:21:51Presenting Commuting_Hermitian in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Commuting_Hermitian" ...
13:21:51Presenting document Commuting_Hermitian/document
13:21:51Presenting document Commuting_Hermitian/outline
13:21:51Presenting theory "HOL-Algebra.Ideal"
13:21:51Presenting theory "Commuting_Hermitian.Commuting_Hermitian_Misc"
13:21:51Presenting theory "Matrix.Matrix_Legacy"
13:21:52Presenting theory "HOL-Algebra.Finite_Extensions"
13:21:52Presenting theory "Multi_Party_Computation.Malicious_OT"
13:21:52Presenting theory "HOL-Algebra.RingHom"
13:21:52Presenting TsirelsonBound in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/TsirelsonBound" ...
13:21:52Presenting document TsirelsonBound/document
13:21:52Presenting document TsirelsonBound/outline
13:21:52Presenting theory "HOL-Algebra.Ring"
13:21:52Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:21:53Presenting theory "Jordan_Normal_Form.Missing_Ring"
13:21:53Presenting theory "Jordan_Normal_Form.Conjugate"
13:21:54Presenting theory "HOL-Algebra.UnivPoly"
13:21:54Presenting theory "HOL-Algebra.Module"
13:21:55Presenting theory "Commuting_Hermitian.Spectral_Theory_Complements"
13:21:55Presenting theory "TsirelsonBound.Tensor_Mat_Compl_Properties"
13:21:55Presenting theory "Perron_Frobenius.Perron_Frobenius_Irreducible"
13:21:55Presenting theory "HOL-Algebra.Generated_Groups"
13:21:55Presenting theory "Stochastic_Matrices.Stochastic_Matrix"
13:21:56Presenting theory "Stochastic_Matrices.Stochastic_Vector_PMF"
13:21:56Presenting theory "HOL-Algebra.Algebraic_Closure"
13:21:56Presenting theory "Stochastic_Matrices.Stochastic_Matrix_Markov_Models"
13:21:56Presenting theory "HOL-Algebra.Elementary_Groups"
13:21:56Presenting theory "TsirelsonBound.Matrix_L2_Operator_Norm"
13:21:56Presenting theory "HOL-Algebra.Left_Coset"
13:21:57Presenting theory "Stochastic_Matrices.Eigenspace"
13:21:57Presenting theory "HOL-Algebra.SimpleGroups"
13:21:57Presenting theory "TsirelsonBound.Density_Matrix_Basics"
13:21:57Presenting theory "HOL-Algebra.SndIsomorphismGrp"
13:21:57Presenting theory "Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius"
13:21:57Presenting theory "HOL-Algebra.Algebra"
13:21:57Presenting Schwartz_Zippel in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Schwartz_Zippel" ...
13:21:57Presenting document Schwartz_Zippel/document
13:21:57Presenting document Schwartz_Zippel/outline
13:21:58Presenting theory "HOL-Computational_Algebra.Squarefree"
13:21:58Presenting theory "HOL-Algebra.Multiplicative_Group"
13:21:59Presenting theory "TsirelsonBound.Tsirelson"
13:21:59Presenting theory "HOL-Library.Groups_Big_Fun"
13:21:59Presenting Universal_Hash_Families in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Universal_Hash_Families" ...
13:21:59Presenting document Universal_Hash_Families/document
13:21:59Presenting document Universal_Hash_Families/outline
13:21:59Presenting theory "Universal_Hash_Families.Universal_Hash_Families"
13:21:59Presenting theory "HOL-Library.Fun_Lexorder"
13:21:59Presenting theory "Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families"
13:21:59Presenting theory "Probabilistic_Prime_Tests.Algebraic_Auxiliaries"
13:21:59Presenting theory "HOL-Algebra.Congruence"
13:21:59Presenting theory "HOL-Number_Theory.Totient"
13:22:00Presenting theory "HOL-Algebra.UnivPoly"
13:22:00Presenting theory "HOL-Algebra.Order"
13:22:01Presenting theory "HOL-Algebra.Lattice"
13:22:01Presenting theory "HOL-Library.More_List"
13:22:01Presenting theory "HOL-Number_Theory.Residues"
13:22:01Presenting theory "Probabilistic_Prime_Tests.Jacobi_Symbol"
13:22:01Presenting theory "Sigma_Commit_Crypto.Number_Theory_Aux"
13:22:01Presenting theory "Jordan_Normal_Form.Matrix"
13:22:02Presenting theory "Probabilistic_Prime_Tests.Residues_Nat"
13:22:02Presenting theory "HOL-Algebra.Complete_Lattice"
13:22:02Presenting theory "Sigma_Commit_Crypto.Uniform_Sampling"
13:22:02Presenting theory "Probabilistic_Prime_Tests.QuadRes"
13:22:02Presenting theory "HOL-Algebra.Generated_Groups"
13:22:03Presenting theory "HOL-Library.More_List"
13:22:03Presenting theory "Sigma_Commit_Crypto.Pedersen"
13:22:03Presenting theory "HOL-Algebra.Group"
13:22:03Presenting theory "Probabilistic_Prime_Tests.Euler_Witness"
13:22:03Presenting theory "HOL-Algebra.Elementary_Groups"
13:22:04Presenting theory "HOL-Algebra.FiniteProduct"
13:22:04Presenting theory "Probabilistic_Prime_Tests.Carmichael_Numbers"
13:22:04Presenting theory "Sigma_Commit_Crypto.Rivest"
13:22:05Presenting theory "HOL-Algebra.Ring"
13:22:05Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:22:06Presenting theory "Sigma_Commit_Crypto.Sigma_Protocols"
13:22:06Presenting theory "Probabilistic_Prime_Tests.Fermat_Witness"
13:22:07Presenting theory "HOL-Algebra.Coset"
13:22:07Presenting theory "Probabilistic_Prime_Tests.Generalized_Primality_Test"
13:22:07Presenting theory "Probabilistic_Prime_Tests.Fermat_Test"
13:22:07Presenting theory "Probabilistic_Prime_Tests.Miller_Rabin_Test"
13:22:07Presenting theory "Sigma_Commit_Crypto.Schnorr_Sigma_Commit"
13:22:07Presenting theory "HOL-Library.Poly_Mapping"
13:22:07Presenting theory "Probabilistic_Prime_Tests.Solovay_Strassen_Test"
13:22:07Presenting theory "HOL-Algebra.Multiplicative_Group"
13:22:07Presenting Prime_Harmonic_Series in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series" ...
13:22:07Presenting document Prime_Harmonic_Series/document
13:22:07Presenting document Prime_Harmonic_Series/outline
13:22:07Presenting theory "HOL-Algebra.AbelCoset"
13:22:08Presenting theory "HOL-Number_Theory.Fib"
13:22:08Presenting theory "HOL-Algebra.Ideal"
13:22:08Presenting theory "HOL-Combinatorics.List_Permutation"
13:22:09Presenting theory "Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit"
13:22:09Presenting theory "HOL-Number_Theory.Totient"
13:22:09Presenting theory "Polynomials.MPoly_Type"
13:22:09Presenting theory "HOL-Number_Theory.Cong"
13:22:10Presenting theory "HOL-Number_Theory.Residues"
13:22:10Presenting theory "Subresultants.Binary_Exponentiation"
13:22:10Presenting theory "HOL-Algebra.Divisibility"
13:22:10Presenting theory "Commuting_Hermitian.Commuting_Hermitian"
13:22:10Presenting theory "HOL-Algebra.Congruence"
13:22:11Presenting theory "Berlekamp_Zassenhaus.Finite_Field"
13:22:11Presenting theory "HOL-Algebra.RingHom"
13:22:11Presenting Schoenhage_Strassen in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Schoenhage_Strassen" ...
13:22:11Presenting document Schoenhage_Strassen/document
13:22:11Presenting document Schoenhage_Strassen/outline
13:22:11Presenting theory "Sigma_Commit_Crypto.Okamoto_Sigma_Commit"
13:22:12Presenting theory "HOL-Algebra.QuotRing"
13:22:12Presenting theory "Sigma_Commit_Crypto.Xor"
13:22:12Presenting theory "HOL-Algebra.Module"
13:22:13Presenting theory "Polynomials.More_MPoly_Type"
13:22:13Presenting theory "Berlekamp_Zassenhaus.Poly_Mod_Finite_Field"
13:22:13Presenting theory "HOL-Algebra.Order"
13:22:13Presenting theory "Sigma_Commit_Crypto.Sigma_AND"
13:22:13Presenting theory "CRYSTALS-Kyber.Kyber_spec"
13:22:14Presenting theory "CRYSTALS-Kyber.Mod_Plus_Minus"
13:22:14Presenting theory "HOL-Algebra.UnivPoly"
13:22:15Presenting theory "HOL-Computational_Algebra.Polynomial"
13:22:15Presenting theory "CRYSTALS-Kyber.Abs_Qr"
13:22:15Presenting theory "HOL-Algebra.Lattice"
13:22:15Presenting theory "HOL-Algebra.Generated_Groups"
13:22:16Presenting theory "HOL-Algebra.Elementary_Groups"
13:22:17Presenting theory "Sigma_Commit_Crypto.Sigma_OR"
13:22:17Presenting Tarskis_Geometry in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry" ...
13:22:17Presenting document Tarskis_Geometry/document
13:22:17Presenting document Tarskis_Geometry/outline
13:22:17Presenting theory "Tarskis_Geometry.Metric"
13:22:17Presenting theory "HOL-Algebra.Multiplicative_Group"
13:22:17Presenting theory "HOL-Computational_Algebra.Fraction_Field"
13:22:18Presenting theory "CRYSTALS-Kyber.Compress"
13:22:18Presenting theory "Tarskis_Geometry.Miscellany"
13:22:18Presenting theory "HOL-Algebra.Ring_Divisibility"
13:22:18Presenting theory "CRYSTALS-Kyber.Crypto_Scheme"
13:22:19Presenting theory "HOL-Algebra.Subrings"
13:22:19Presenting theory "HOL-Eisbach.Eisbach"
13:22:19Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
13:22:19Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
13:22:19Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
13:22:19Presenting file "~~/src/HOL/Eisbach/match_method.ML"
13:22:19Presenting theory "Expander_Graphs.Extra_Congruence_Method"
13:22:19Presenting theory "Tarskis_Geometry.Tarski"
13:22:19Presenting theory "CRYSTALS-Kyber_Security.Crypto_Scheme_new"
13:22:19Presenting theory "CRYSTALS-Kyber_Security.Delta_Correct"
13:22:19Presenting theory "CRYSTALS-Kyber_Security.Finite_UNIV"
13:22:19Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
13:22:19Presenting theory "HOL-Algebra.Complete_Lattice"
13:22:19Presenting theory "CRYSTALS-Kyber_Security.Lemmas_for_spmf"
13:22:20Presenting theory "CRYSTALS-Kyber_Security.MLWE"
13:22:21Presenting theory "HOL-Number_Theory.Cong"
13:22:21Presenting theory "HOL-Algebra.Polynomials"
13:22:21Presenting theory "CRYSTALS-Kyber_Security.Correct_new"
13:22:22Presenting theory "HOL-Algebra.Congruence"
13:22:22Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
13:22:22Presenting theory "Tarskis_Geometry.Euclid_Tarski"
13:22:23Presenting theory "Tarskis_Geometry.Linear_Algebra2"
13:22:23Presenting theory "HOL-Algebra.Order"
13:22:23Presenting theory "HOL-Algebra.Embedded_Algebras"
13:22:24Presenting theory "Matrix_Tensor.Matrix_Tensor"
13:22:24Presenting theory "HOL-Algebra.Congruence"
13:22:24Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:22:25Presenting theory "HOL-Algebra.Lattice"
13:22:25Presenting theory "HOL-Algebra.Group"
13:22:25Presenting theory "HOL-Algebra.Order"
13:22:26Presenting theory "HOL-Algebra.Polynomial_Divisibility"
13:22:26Presenting theory "Isabelle_Marries_Dirac.Tensor"
13:22:26Presenting theory "Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials"
13:22:27Presenting theory "Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation"
13:22:27Presenting theory "Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities"
13:22:27Presenting theory "HOL-Algebra.Lattice"
13:22:27Presenting theory "Universal_Hash_Families.Carter_Wegman_Hash_Family"
13:22:27Presenting theory "HOL-Library.Function_Algebras"
13:22:28Presenting theory "Isabelle_Marries_Dirac.More_Tensor"
13:22:29Presenting theory "Ergodic_Theory.SG_Library_Complement"
13:22:29Presenting theory "HOL-Algebra.Complete_Lattice"
13:22:29Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:22:30Presenting theory "Lp.Functional_Spaces"
13:22:30Presenting theory "Polynomial_Factorization.Order_Polynomial"
13:22:30Presenting theory "HOL-Algebra.Complete_Lattice"
13:22:30Presenting theory "HOL-Algebra.Coset"
13:22:32Presenting theory "HOL-Algebra.FiniteProduct"
13:22:34Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
13:22:34Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
13:22:34Presenting theory "Lp.Lp"
13:22:35Presenting theory "Concentration_Inequalities.Concentration_Inequalities_Preliminary"
13:22:35Presenting theory "HOL-Algebra.Group"
13:22:35Presenting theory "HOL-Algebra.Group"
13:22:35Presenting theory "HOL-Algebra.Ring"
13:22:35Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:22:35Presenting theory "Tarskis_Geometry.Action"
13:22:35Presenting theory "HOL-Computational_Algebra.Polynomial"
13:22:35Presenting theory "Digit_Expansions.Bits_Digits"
13:22:36Presenting theory "Finite_Fields.Finite_Fields_More_Bijections"
13:22:36Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:22:36Presenting theory "Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF"
13:22:36Presenting theory "HOL-Algebra.Module"
13:22:36Presenting theory "Universal_Hash_Families.Pseudorandom_Objects"
13:22:36Presenting theory "Finite_Fields.Finite_Fields_More_PMF"
13:22:36Presenting theory "Finite_Fields.Finite_Fields_Indexed_Algebra_Code"
13:22:37Presenting theory "QHLProver.Complex_Matrix"
13:22:37Presenting theory "Polynomials.MPoly_Type_Univariate"
13:22:37Presenting file "$AFP/QHLProver/mat_alg.ML"
13:22:37Presenting theory "Finite_Fields.Finite_Fields_Preliminary_Results"
13:22:37Presenting theory "QHLProver.Gates"
13:22:38Presenting theory "HOL-Types_To_Sets.Prerequisites"
13:22:38Presenting theory "Finite_Fields.Finite_Fields_Factorization_Ext"
13:22:38Presenting theory "HOL-Algebra.AbelCoset"
13:22:38Presenting theory "Jordan_Normal_Form.Missing_Misc"
13:22:38Presenting theory "HOL-Algebra.IntRing"
13:22:38Presenting theory "CRYSTALS-Kyber_Security.Kyber_gpv_IND_CPA"
13:22:39Presenting theory "CRYSTALS-Kyber_Security.Kyber_new_Values"
13:22:39Presenting theory "Finite_Fields.Ring_Characteristic"
13:22:39Presenting theory "Finite_Fields.Formal_Polynomial_Derivatives"
13:22:40Presenting theory "HOL-Algebra.Coset"
13:22:40Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:22:40Presenting theory "Finite_Fields.Monic_Polynomial_Factorization"
13:22:40Presenting theory "HOL-Algebra.Ideal"
13:22:41Presenting theory "HOL-Types_To_Sets.Group_On_With"
13:22:41Presenting theory "Finite_Fields.Card_Irreducible_Polynomials_Aux"
13:22:41Presenting theory "HOL-Algebra.RingHom"
13:22:41Presenting theory "HOL-Algebra.FiniteProduct"
13:22:41Presenting theory "CRYSTALS-Kyber_Security.Correct"
13:22:41Presenting Matrix in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Matrix" ...
13:22:41Presenting document Matrix/document
13:22:41Presenting document Matrix/outline
13:22:41Presenting theory "HOL-Computational_Algebra.Fraction_Field"
13:22:42Presenting theory "Finite_Fields.Finite_Fields_Poly_Ring_Code"
13:22:42Presenting theory "Matrix.Utility"
13:22:42Presenting theory "Finite_Fields.Finite_Fields_Mod_Ring_Code"
13:22:42Presenting theory "Finite_Fields.Rabin_Irreducibility_Test"
13:22:42Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
13:22:43Presenting theory "Finite_Fields.Rabin_Irreducibility_Test_Code"
13:22:43Presenting theory "HOL-Algebra.Congruence"
13:22:43Presenting theory "Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code"
13:22:44Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
13:22:44Presenting theory "HOL-Library.Transitive_Closure_Table"
13:22:44Presenting theory "HOL-Algebra.Ring"
13:22:44Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:22:44Presenting theory "Tarskis_Geometry.Projective"
13:22:44Presenting theory "HOL-Library.While_Combinator"
13:22:44Presenting theory "Jordan_Normal_Form.Column_Operations"
13:22:45Presenting theory "HOL-Library.Bourbaki_Witt_Fixpoint"
13:22:45Presenting theory "HOL-Algebra.Order"
13:22:45Presenting theory "MFMC_Countable.MFMC_Misc"
13:22:45Presenting theory "HOL-Algebra.Module"
13:22:45Presenting theory "HOL-Library.Quadratic_Discriminant"
13:22:46Presenting theory "Flow_Networks.Graph"
13:22:46Presenting theory "Flow_Networks.Network"
13:22:46Presenting theory "Flow_Networks.Residual_Graph"
13:22:46Presenting theory "HOL-Algebra.Lattice"
13:22:46Presenting theory "Flow_Networks.Augmenting_Flow"
13:22:47Presenting theory "Flow_Networks.Augmenting_Path"
13:22:47Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
13:22:47Presenting theory "HOL-Algebra.AbelCoset"
13:22:47Presenting theory "Flow_Networks.Ford_Fulkerson"
13:22:47Presenting theory "EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract"
13:22:47Presenting theory "Projective_Measurements.Linear_Algebra_Complements"
13:22:47Presenting theory "MFMC_Countable.MFMC_Finite"
13:22:48Presenting theory "MFMC_Countable.Matrix_For_Marginals"
13:22:49Presenting theory "MFMC_Countable.Rel_PMF_Characterisation"
13:22:49Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:22:49Presenting theory "HOL-Algebra.Ideal"
13:22:49Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:22:49Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:22:49Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:22:49Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:22:49Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:22:49Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:22:49Presenting theory "HOL-Algebra.Complete_Lattice"
13:22:49Presenting theory "HOL-Algebra.RingHom"
13:22:50Presenting theory "Probabilistic_While.While_SPMF"
13:22:50Presenting theory "HOL-Number_Theory.Fib"
13:22:50Presenting theory "HOL-Algebra.UnivPoly"
13:22:51Presenting theory "HOL-Number_Theory.Cong"
13:22:51Presenting theory "HOL-Number_Theory.Totient"
13:22:52Presenting theory "HOL-Number_Theory.Residues"
13:22:52Presenting theory "HOL-Number_Theory.Eratosthenes"
13:22:52Presenting theory "HOL-Library.Power_By_Squaring"
13:22:52Presenting theory "HOL-Number_Theory.Mod_Exp"
13:22:52Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:22:53Presenting theory "Projective_Measurements.Projective_Measurements"
13:22:53Presenting theory "HOL-Number_Theory.Gauss"
13:22:53Presenting theory "HOL-Algebra.Group"
13:22:53Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:22:53Presenting theory "HOL-Algebra.Generated_Groups"
13:22:54Presenting theory "HOL-Number_Theory.Pocklington"
13:22:55Presenting theory "HOL-Number_Theory.Prime_Powers"
13:22:55Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:22:55Presenting theory "HOL-Algebra.FiniteProduct"
13:22:55Presenting theory "HOL-Algebra.Elementary_Groups"
13:22:55Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:22:56Presenting theory "HOL-Number_Theory.Number_Theory"
13:22:56Presenting theory "HOL-Computational_Algebra.Squarefree"
13:22:56Presenting theory "Dirichlet_Series.Dirichlet_Misc"
13:22:56Presenting theory "Dirichlet_Series.Multiplicative_Function"
13:22:56Presenting theory "Commuting_Hermitian.Spectral_Theory_Complements"
13:22:57Presenting theory "Dirichlet_Series.Dirichlet_Product"
13:22:57Presenting theory "Jordan_Normal_Form.Determinant"
13:22:57Presenting theory "Commuting_Hermitian.Commuting_Hermitian_Misc"
13:22:57Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:22:57Presenting theory "HOL-Library.More_List"
13:22:58Presenting theory "Polynomial_Factorization.Order_Polynomial"
13:22:58Presenting theory "HOL-Algebra.UnivPoly"
13:22:59Presenting theory "HOL-Algebra.Ring"
13:22:59Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:22:59Presenting theory "Matrix.Ordered_Semiring"
13:22:59Presenting theory "HOL-Algebra.Multiplicative_Group"
13:23:01Presenting theory "Tarskis_Geometry.Hyperbolic_Tarski"
13:23:01Presenting theory "Jordan_Normal_Form.Char_Poly"
13:23:01Presenting theory "HOL-Number_Theory.Totient"
13:23:01Presenting theory "HOL-Algebra.Generated_Groups"
13:23:01Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
13:23:02Presenting Matrix_Tensor in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Matrix_Tensor" ...
13:23:02Presenting document Matrix_Tensor/document
13:23:02Presenting document Matrix_Tensor/outline
13:23:02Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
13:23:02Presenting theory "HOL-Computational_Algebra.Polynomial"
13:23:02Presenting theory "HOL-Number_Theory.Residues"
13:23:02Presenting theory "HOL-Algebra.Elementary_Groups"
13:23:02Presenting theory "Matrix.Matrix_Legacy"
13:23:03Presenting theory "HOL-Computational_Algebra.Polynomial_FPS"
13:23:03Presenting theory "HOL-Number_Theory.Eratosthenes"
13:23:03Presenting Knot_Theory in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Knot_Theory" ...
13:23:03Presenting document Knot_Theory/document
13:23:03Presenting document Knot_Theory/outline
13:23:03Presenting theory "HOL-Computational_Algebra.Polynomial_FPS"
13:23:03Presenting theory "HOL-Library.Power_By_Squaring"
13:23:03Presenting theory "Knot_Theory.Preliminaries"
13:23:03Presenting theory "HOL-Number_Theory.Mod_Exp"
13:23:04Presenting theory "Knot_Theory.Tangles"
13:23:04Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:23:05Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form"
13:23:05Presenting theory "Isabelle_Marries_Dirac.Basics"
13:23:05Presenting theory "HOL-Number_Theory.Gauss"
13:23:06Presenting theory "HOL-Computational_Algebra.Formal_Laurent_Series"
13:23:06Presenting theory "HOL-Algebra.Multiplicative_Group"
13:23:06Presenting theory "Isabelle_Marries_Dirac.Binary_Nat"
13:23:07Presenting theory "HOL-Computational_Algebra.Fraction_Field"
13:23:07Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:23:07Presenting theory "Knot_Theory.Tangle_Algebra"
13:23:08Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
13:23:08Presenting theory "Knot_Theory.Tangle_Relation"
13:23:08Presenting theory "HOL-Computational_Algebra.Group_Closure"
13:23:08Presenting theory "HOL-Number_Theory.Totient"
13:23:08Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
13:23:08Presenting theory "HOL-Computational_Algebra.Nth_Powers"
13:23:09Presenting theory "Knot_Theory.Tangle_Moves"
13:23:09Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
13:23:09Presenting theory "Commuting_Hermitian.Commuting_Hermitian"
13:23:09Presenting theory "HOL-Computational_Algebra.Computational_Algebra"
13:23:09Presenting theory "Knot_Theory.Link_Algebra"
13:23:09Presenting theory "HOL-Number_Theory.Residues"
13:23:10Presenting theory "Karatsuba.Karatsuba_Preliminaries"
13:23:11Presenting theory "Dirichlet_Series.Dirichlet_Series"
13:23:11Presenting theory "HOL-Number_Theory.Pocklington"
13:23:11Presenting theory "Karatsuba.Karatsuba_Sum_Lemmas"
13:23:11Presenting theory "Karatsuba.Abstract_Representations"
13:23:11Presenting theory "Dirichlet_Series.Moebius_Mu"
13:23:12Presenting theory "Isabelle_Marries_Dirac.Quantum"
13:23:12Presenting theory "HOL-Library.Log_Nat"
13:23:12Presenting theory "Finite_Fields.Card_Irreducible_Polynomials"
13:23:12Presenting theory "HOL-Library.Case_Converter"
13:23:12Presenting file "~~/src/HOL/Library/case_converter.ML"
13:23:13Presenting theory "HOL-Number_Theory.Prime_Powers"
13:23:13Presenting theory "Expander_Graphs.Expander_Graphs_Eigenvalues"
13:23:13Presenting theory "HOL-Library.Code_Lazy"
13:23:13Presenting file "~~/src/HOL/Library/code_lazy.ML"
13:23:14Presenting theory "Executable_Randomized_Algorithms.Coin_Space"
13:23:14Presenting theory "Executable_Randomized_Algorithms.Tau_Additivity"
13:23:15Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:23:15Presenting theory "HOL-Number_Theory.Number_Theory"
13:23:15Presenting theory "Knot_Theory.Example"
13:23:15Presenting theory "Prime_Harmonic_Series.Prime_Harmonic_Misc"
13:23:15Presenting theory "Expander_Graphs.Expander_Graphs_Cheeger_Inequality"
13:23:16Presenting theory "Prime_Harmonic_Series.Squarefree_Nat"
13:23:16Presenting theory "Prime_Harmonic_Series.Prime_Harmonic"
13:23:17Presenting theory "HOL-Library.Lattice_Algebras"
13:23:17Presenting theory "HOL-Complex_Analysis.Contour_Integration"
13:23:17Presenting HOL-Algebra in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Algebra" ...
13:23:17Presenting document HOL-Algebra/document
13:23:17Presenting document HOL-Algebra/outline
13:23:17Presenting theory "HOL-Algebra.README"
13:23:17Presenting theory "Karatsuba.Nat_LSBF"
13:23:17Presenting theory "HOL-Algebra.Congruence"
13:23:18Presenting theory "Schoenhage_Strassen.Schoenhage_Strassen_Preliminaries"
13:23:18Presenting theory "HOL-Library.Interval"
13:23:18Presenting theory "HOL-Library.Adhoc_Overloading"
13:23:18Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
13:23:18Presenting theory "HOL-Library.Monad_Syntax"
13:23:18Presenting theory "HOL-Library.Log_Nat"
13:23:19Presenting theory "Root_Balanced_Tree.Time_Monad"
13:23:19Presenting theory "Karatsuba.Time_Monad_Extended"
13:23:19Presenting theory "HOL-Algebra.Order"
13:23:19Presenting theory "HOL-Computational_Algebra.Formal_Laurent_Series"
13:23:19Presenting theory "HOL-Eisbach.Eisbach_Tools"
13:23:19Presenting theory "HOL-Computational_Algebra.Factorial_Ring"
13:23:19Presenting theory "Karatsuba.Estimation_Method"
13:23:19Presenting theory "HOL-Complex_Analysis.Cauchy_Integral_Theorem"
13:23:20Presenting theory "HOL-Algebra.Lattice"
13:23:20Presenting theory "HOL-Computational_Algebra.Euclidean_Algorithm"
13:23:20Presenting theory "HOL-Computational_Algebra.Group_Closure"
13:23:21Presenting theory "HOL-Algebra.Coset"
13:23:21Presenting theory "HOL-Computational_Algebra.Primes"
13:23:21Presenting theory "Karatsuba.Main_TM"
13:23:21Presenting theory "HOL-Computational_Algebra.Nth_Powers"
13:23:21Presenting theory "HOL-Library.Function_Algebras"
13:23:22Presenting theory "VectorSpace.RingModuleFacts"
13:23:22Presenting theory "VectorSpace.FunctionLemmas"
13:23:22Presenting theory "HOL-Algebra.Complete_Lattice"
13:23:22Presenting theory "VectorSpace.MonoidSums"
13:23:22Presenting theory "HOL-Algebra.Galois_Connection"
13:23:23Presenting theory "HOL-Computational_Algebra.Squarefree"
13:23:23Presenting theory "HOL-Computational_Algebra.Computational_Algebra"
13:23:23Presenting theory "HOL-Library.Float"
13:23:23Presenting theory "Landau_Symbols.Group_Sort"
13:23:24Presenting theory "HOL-Library.Interval_Float"
13:23:24Presenting theory "Symmetric_Polynomials.Vieta"
13:23:25Presenting theory "HOL-Algebra.Group"
13:23:26Presenting theory "Matrix_Tensor.Matrix_Tensor"
13:23:27Presenting theory "VectorSpace.LinearCombinations"
13:23:27Presenting Finite_Fields in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Finite_Fields" ...
13:23:27Presenting theory "HOL-Algebra.FiniteProduct"
13:23:27Presenting document Finite_Fields/document
13:23:27Presenting document Finite_Fields/outline
13:23:27Presenting theory "HOL-Computational_Algebra.Polynomial"
13:23:27Presenting theory "HOL-Number_Theory.Fib"
13:23:28Presenting theory "VectorSpace.SumSpaces"
13:23:28Presenting theory "HOL-Complex_Analysis.Winding_Numbers"
13:23:28Presenting theory "Landau_Symbols.Landau_Real_Products"
13:23:28Presenting theory "HOL-Number_Theory.Cong"
13:23:28Presenting theory "HOL-Decision_Procs.Dense_Linear_Order"
13:23:28Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML"
13:23:28Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML"
13:23:28Presenting file "~~/src/HOL/Decision_Procs/langford.ML"
13:23:28Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"
13:23:29Presenting theory "HOL-Computational_Algebra.Fraction_Field"
13:23:29Presenting theory "Landau_Symbols.Landau_Simprocs"
13:23:30Presenting file "$AFP/Landau_Symbols/landau_simprocs.ML"
13:23:30Presenting theory "HOL-Number_Theory.Totient"
13:23:30Presenting theory "Landau_Symbols.Landau_More"
13:23:30Presenting theory "Pure-ex.Guess"
13:23:30Presenting theory "Akra_Bazzi.Akra_Bazzi_Library"
13:23:31Presenting theory "HOL-Number_Theory.Residues"
13:23:31Presenting theory "Akra_Bazzi.Akra_Bazzi_Asymptotics"
13:23:32Presenting theory "Knot_Theory.Kauffman_Matrix"
13:23:32Presenting theory "HOL-Number_Theory.Eratosthenes"
13:23:32Presenting theory "HOL-Number_Theory.Mod_Exp"
13:23:32Presenting theory "HOL-Algebra.Coset"
13:23:33Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:23:33Presenting theory "VectorSpace.VectorSpace"
13:23:33Presenting theory "HOL-Algebra.Exponent"
13:23:33Presenting theory "Akra_Bazzi.Akra_Bazzi_Real"
13:23:34Presenting theory "HOL-Number_Theory.Gauss"
13:23:34Presenting theory "HOL-Algebra.Sylow"
13:23:34Presenting theory "Knot_Theory.Computations"
13:23:34Presenting theory "Isabelle_Marries_Dirac.Complex_Vectors"
13:23:35Presenting theory "HOL-Algebra.Bij"
13:23:35Presenting theory "Akra_Bazzi.Akra_Bazzi"
13:23:35Presenting theory "Knot_Theory.Linkrel_Kauffman"
13:23:35Presenting theory "Matrix.Utility"
13:23:35Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:23:35Presenting theory "Knot_Theory.Kauffman_Invariance"
13:23:35Presenting theory "Knot_Theory.Knot_Theory"
13:23:35Presenting Finitely_Generated_Abelian_Groups in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Finitely_Generated_Abelian_Groups" ...
13:23:36Presenting document Finitely_Generated_Abelian_Groups/document
13:23:36Presenting document Finitely_Generated_Abelian_Groups/outline
13:23:36Presenting theory "Akra_Bazzi.Master_Theorem"
13:23:36Presenting theory "Finitely_Generated_Abelian_Groups.Set_Multiplication"
13:23:36Presenting theory "Akra_Bazzi.Eval_Numeral"
13:23:36Presenting theory "Finitely_Generated_Abelian_Groups.Miscellaneous_Groups"
13:23:36Presenting theory "Finitely_Generated_Abelian_Groups.Generated_Groups_Extend"
13:23:37Presenting theory "Finitely_Generated_Abelian_Groups.General_Auxiliary"
13:23:37Presenting theory "HOL-Complex_Analysis.Cauchy_Integral_Formula"
13:23:37Presenting theory "Regular-Sets.Regular_Set"
13:23:37Presenting theory "Finitely_Generated_Abelian_Groups.IDirProds"
13:23:37Presenting theory "Akra_Bazzi.Akra_Bazzi_Method"
13:23:37Presenting file "$AFP/Akra_Bazzi/akra_bazzi.ML"
13:23:38Presenting theory "HOL-Decision_Procs.Approximation_Bounds"
13:23:38Presenting theory "Regular-Sets.Regular_Exp"
13:23:38Presenting theory "Karatsuba.Karatsuba_Runtime_Lemmas"
13:23:38Presenting theory "Regular-Sets.NDerivative"
13:23:38Presenting theory "HOL-Number_Theory.Pocklington"
13:23:38Presenting theory "Finitely_Generated_Abelian_Groups.Finite_Product_Extend"
13:23:39Presenting theory "Karatsuba.Nat_LSBF_TM"
13:23:39Presenting theory "HOL-Library.Code_Target_Int"
13:23:39Presenting theory "HOL-Algebra.Ring"
13:23:39Presenting theory "Finitely_Generated_Abelian_Groups.Group_Hom"
13:23:39Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:23:39Presenting theory "HOL-Library.Code_Abstract_Nat"
13:23:39Presenting theory "HOL-Library.While_Combinator"
13:23:39Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
13:23:39Presenting theory "HOL-Library.Code_Target_Nat"
13:23:39Presenting theory "Schoenhage_Strassen.Schoenhage_Strassen_Runtime_Preliminaries"
13:23:39Presenting theory "HOL-Library.Code_Target_Numeral"
13:23:39Presenting theory "HOL-Library.Code_Target_Numeral_Float"
13:23:39Presenting theory "Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups"
13:23:39Presenting theory "Schoenhage_Strassen.Schoenhage_Strassen_Ring_Lemmas"
13:23:40Presenting theory "Subresultants.Binary_Exponentiation"
13:23:40Presenting theory "HOL-Algebra.Module"
13:23:40Presenting theory "HOL-Number_Theory.Prime_Powers"
13:23:40Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:23:40Presenting theory "Regular-Sets.Equivalence_Checking"
13:23:40Presenting theory "Regular-Sets.Relation_Interpretation"
13:23:41Presenting theory "HOL-Algebra.AbelCoset"
13:23:41Presenting theory "Regular-Sets.Regexp_Method"
13:23:41Presenting theory "Finitely_Generated_Abelian_Groups.DirProds"
13:23:41Presenting theory "HOL-Library.More_List"
13:23:42Presenting theory "Abstract-Rewriting.Seq"
13:23:42Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
13:23:42Presenting theory "HOL-Algebra.Ideal"
13:23:42Presenting theory "HOL-Decision_Procs.Approximation"
13:23:42Presenting theory "Finitely_Generated_Abelian_Groups.Group_Relations"
13:23:42Presenting file "~~/src/HOL/Decision_Procs/approximation.ML"
13:23:42Presenting file "~~/src/HOL/Decision_Procs/approximation_generator.ML"
13:23:42Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:23:42Presenting theory "HOL-Algebra.RingHom"
13:23:42Presenting theory "HOL-Number_Theory.Number_Theory"
13:23:43Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
13:23:43Presenting theory "Dirichlet_Series.Dirichlet_Misc"
13:23:44Presenting theory "HOL-Complex_Analysis.Conformal_Mappings"
13:23:44Presenting theory "Dirichlet_Series.Multiplicative_Function"
13:23:46Presenting theory "Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups"
13:23:46Presenting Groebner_Bases in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Groebner_Bases" ...
13:23:46Presenting document Groebner_Bases/document
13:23:46Presenting document Groebner_Bases/outline
13:23:47Presenting theory "HOL-Algebra.UnivPoly"
13:23:47Presenting theory "HOL-Computational_Algebra.Polynomial"
13:23:47Presenting theory "Regular-Sets.Regular_Set"
13:23:47Presenting theory "Dirichlet_Series.Dirichlet_Product"
13:23:47Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
13:23:47Presenting theory "Regular-Sets.Regular_Exp"
13:23:47Presenting theory "Expander_Graphs.Expander_Graphs_MGG"
13:23:47Presenting theory "Regular-Sets.NDerivative"
13:23:47Presenting theory "HOL-Library.Ramsey"
13:23:48Presenting theory "Abstract-Rewriting.SN_Orders"
13:23:48Presenting theory "Matrix.Ordered_Semiring"
13:23:48Presenting theory "Regular-Sets.Equivalence_Checking"
13:23:48Presenting theory "Regular-Sets.Relation_Interpretation"
13:23:48Presenting theory "Regular-Sets.Regexp_Method"
13:23:49Presenting theory "Dirichlet_Series.Dirichlet_Series"
13:23:49Presenting theory "Regular-Sets.Regular_Set"
13:23:49Presenting theory "HOL-Computational_Algebra.Fraction_Field"
13:23:49Presenting theory "Expander_Graphs.Expander_Graphs_Walks"
13:23:49Presenting theory "HOL-Algebra.Generated_Groups"
13:23:49Presenting theory "Matrix.Matrix_Legacy"
13:23:49Presenting theory "Regular-Sets.Regular_Exp"
13:23:49Presenting theory "Dirichlet_Series.Moebius_Mu"
13:23:50Presenting theory "Regular-Sets.NDerivative"
13:23:50Presenting theory "HOL-Algebra.Elementary_Groups"
13:23:50Presenting theory "Abstract-Rewriting.Seq"
13:23:50Presenting theory "Well_Quasi_Orders.Least_Enum"
13:23:51Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
13:23:51Presenting theory "HOL-Complex_Analysis.Great_Picard"
13:23:51Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
13:23:51Presenting theory "HOL-Library.While_Combinator"
13:23:52Presenting theory "HOL-Algebra.Multiplicative_Group"
13:23:52Presenting theory "Finite_Fields.Finite_Fields_Preliminary_Results"
13:23:52Presenting theory "Expander_Graphs.Expander_Graphs_Power_Construction"
13:23:53Presenting theory "Regular-Sets.Equivalence_Checking"
13:23:53Presenting theory "HOL-Algebra.Group_Action"
13:23:53Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
13:23:53Presenting theory "Open_Induction.Restricted_Predicates"
13:23:53Presenting theory "Regular-Sets.Relation_Interpretation"
13:23:53Presenting theory "Finite_Fields.Finite_Fields_Factorization_Ext"
13:23:53Presenting theory "Regular-Sets.Regexp_Method"
13:23:54Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:23:55Presenting theory "HOL-Algebra.Zassenhaus"
13:23:55Presenting theory "HOL-Complex_Analysis.Riemann_Mapping"
13:23:55Presenting theory "Well_Quasi_Orders.Almost_Full"
13:23:55Presenting theory "HOL-Combinatorics.Transposition"
13:23:56Presenting theory "Abstract-Rewriting.Seq"
13:23:56Presenting theory "Well_Quasi_Orders.Minimal_Elements"
13:23:56Presenting theory "Finite_Fields.Ring_Characteristic"
13:23:56Presenting theory "Well_Quasi_Orders.Least_Enum"
13:23:56Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
13:23:56Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
13:23:57Presenting theory "Expander_Graphs.Expander_Graphs_Strongly_Explicit"
13:23:57Presenting theory "Finite_Fields.Formal_Polynomial_Derivatives"
13:23:58Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
13:23:58Presenting theory "Universal_Hash_Families.Pseudorandom_Objects"
13:23:58Presenting theory "HOL-Complex_Analysis.Complex_Singularities"
13:23:58Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:23:59Presenting theory "Finite_Fields.Monic_Polynomial_Factorization"
13:23:59Presenting theory "Open_Induction.Restricted_Predicates"
13:23:59Presenting theory "HOL-Complex_Analysis.Complex_Residues"
13:23:59Presenting theory "Expander_Graphs.Pseudorandom_Objects_Expander_Walks"
13:23:59Presenting Groebner_Macaulay in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Groebner_Macaulay" ...
13:23:59Presenting document Groebner_Macaulay/document
13:23:59Presenting document Groebner_Macaulay/outline
13:23:59Presenting theory "Polynomials.Utils"
13:24:00Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:24:00Presenting theory "HOL-Combinatorics.Permutations"
13:24:00Presenting theory "Matrix_Tensor.Matrix_Tensor"
13:24:00Presenting theory "HOL-Combinatorics.List_Permutation"
13:24:00Presenting theory "HOL-Complex_Analysis.Residue_Theorem"
13:24:01Presenting theory "Berlekamp_Zassenhaus.Finite_Field"
13:24:01Presenting theory "Groebner_Macaulay.Degree_Section"
13:24:01Presenting theory "Finite_Fields.Card_Irreducible_Polynomials_Aux"
13:24:01Presenting theory "Well_Quasi_Orders.Almost_Full"
13:24:01Presenting theory "Isabelle_Marries_Dirac.Tensor"
13:24:01Presenting theory "HOL-Number_Theory.Fib"
13:24:02Presenting theory "Finite_Fields.Card_Irreducible_Polynomials"
13:24:02Presenting theory "Well_Quasi_Orders.Minimal_Elements"
13:24:02Presenting theory "HOL-Number_Theory.Eratosthenes"
13:24:02Presenting theory "HOL-Library.Power_By_Squaring"
13:24:03Presenting theory "HOL-Number_Theory.Mod_Exp"
13:24:03Presenting theory "Groebner_Bases.General"
13:24:03Presenting theory "HOL-Complex_Analysis.Laurent_Convergence"
13:24:03Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:24:03Presenting theory "Finite_Fields.Finite_Fields_Isomorphic"
13:24:03Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
13:24:03Presenting theory "Groebner_Macaulay.Degree_Bound_Utils"
13:24:03Presenting theory "Isabelle_Marries_Dirac.More_Tensor"
13:24:03Presenting theory "HOL-Number_Theory.Gauss"
13:24:04Presenting theory "Polynomials.MPoly_Type"
13:24:04Presenting theory "Groebner_Macaulay.Groebner_Macaulay"
13:24:04Presenting theory "Finite_Fields.Rabin_Irreducibility_Test"
13:24:04Presenting theory "HOL-Complex_Analysis.Meromorphic"
13:24:04Presenting theory "Groebner_Macaulay.Binomial_Int"
13:24:04Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:24:04Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
13:24:04Presenting theory "Finite_Fields.Finite_Fields_Indexed_Algebra_Code"
13:24:05Presenting theory "Polynomials.More_MPoly_Type"
13:24:05Presenting theory "Groebner_Macaulay.Poly_Fun"
13:24:05Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
13:24:06Presenting theory "HOL-Complex_Analysis.Weierstrass_Factorization"
13:24:06Presenting theory "HOL-Complex_Analysis.Complex_Analysis"
13:24:06Presenting theory "HOL-Library.Going_To_Filter"
13:24:06Presenting theory "Dirichlet_Series.More_Totient"
13:24:06Presenting theory "Finite_Fields.Finite_Fields_Poly_Ring_Code"
13:24:06Presenting theory "Dirichlet_Series.Liouville_Lambda"
13:24:06Presenting theory "Polynomials.Utils"
13:24:07Presenting theory "Dirichlet_Series.Divisor_Count"
13:24:07Presenting theory "Groebner_Macaulay.Monomial_Module"
13:24:07Presenting theory "HOL-Number_Theory.Pocklington"
13:24:07Presenting theory "HOL-Library.Function_Algebras"
13:24:07Presenting theory "Dirichlet_Series.Arithmetic_Summatory"
13:24:07Presenting theory "Finite_Fields.Finite_Fields_Mod_Ring_Code"
13:24:07Presenting theory "Dirichlet_Series.Partial_Summation"
13:24:07Presenting theory "Dirichlet_Series.Euler_Products"
13:24:07Presenting theory "Groebner_Macaulay.Dube_Prelims"
13:24:08Presenting theory "HOL-Algebra.Divisibility"
13:24:08Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
13:24:08Presenting theory "Finite_Fields.Rabin_Irreducibility_Test_Code"
13:24:09Presenting theory "Jordan_Normal_Form.Missing_VectorSpace"
13:24:09Presenting theory "HOL-Number_Theory.Prime_Powers"
13:24:10Presenting theory "Digit_Expansions.Bits_Digits"
13:24:10Presenting theory "Dirichlet_Series.Dirichlet_Series_Analysis"
13:24:11Presenting theory "HOL-Algebra.QuotRing"
13:24:11Presenting theory "Finite_Fields.Finite_Fields_More_Bijections"
13:24:11Presenting theory "HOL-Analysis.L2_Norm"
13:24:11Presenting theory "HOL-Algebra.IntRing"
13:24:12Presenting theory "HOL-Analysis.Inner_Product"
13:24:12Presenting theory "Groebner_Macaulay.Hilbert_Function"
13:24:12Presenting theory "Zeta_Function.Zeta_Library"
13:24:12Presenting theory "Polynomials.Power_Products"
13:24:12Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:24:13Presenting theory "HOL-Number_Theory.Number_Theory"
13:24:13Presenting theory "Jordan_Normal_Form.VS_Connect"
13:24:13Presenting theory "HOL-Algebra.Weak_Morphisms"
13:24:14Presenting theory "HOL-Analysis.Product_Vector"
13:24:14Presenting theory "Polynomials.Power_Products"
13:24:14Presenting theory "Polynomials.More_Modules"
13:24:14Presenting theory "Number_Theoretic_Transform.Preliminary_Lemmas"
13:24:14Presenting theory "HOL-Algebra.Ring_Divisibility"
13:24:14Presenting theory "Polynomials.More_Modules"
13:24:15Presenting theory "HOL-Analysis.Euclidean_Space"
13:24:15Presenting theory "HOL-Algebra.Subrings"
13:24:15Presenting theory "Jordan_Normal_Form.Gram_Schmidt"
13:24:15Presenting theory "Number_Theoretic_Transform.NTT"
13:24:16Presenting theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal"
13:24:16Presenting theory "Jordan_Normal_Form.Schur_Decomposition"
13:24:16Presenting theory "Polynomials.MPoly_Type_Class"
13:24:17Presenting theory "Executable_Randomized_Algorithms.Randomized_Algorithm"
13:24:17Presenting theory "Karatsuba.Monoid_Sums"
13:24:17Presenting theory "HOL-Library.Log_Nat"
13:24:18Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
13:24:18Presenting theory "HOL-Analysis.Linear_Algebra"
13:24:18Presenting theory "Schwartz_Zippel.Schwartz_Zippel"
13:24:18Presenting theory "Finite_Fields.Find_Irreducible_Poly"
13:24:19Presenting theory "Schoenhage_Strassen.NTT_Rings"
13:24:19Presenting theory "HOL-Algebra.Congruence"
13:24:19Presenting theory "Polynomials.MPoly_Type_Class"
13:24:20Presenting theory "HOL-Algebra.Order"
13:24:20Presenting theory "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families"
13:24:20Presenting Nullstellensatz in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Nullstellensatz" ...
13:24:20Presenting document Nullstellensatz/document
13:24:20Presenting document Nullstellensatz/outline
13:24:20Presenting theory "HOL-Analysis.Affine"
13:24:21Presenting theory "HOL-Algebra.Lattice"
13:24:21Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:24:21Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:24:21Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:24:21Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:24:21Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:24:21Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:24:22Presenting theory "HOL-Algebra.Polynomials"
13:24:22Presenting theory "Number_Theoretic_Transform.Butterfly"
13:24:22Presenting theory "Nullstellensatz.Algebraically_Closed_Fields"
13:24:22Presenting theory "Nullstellensatz.Lex_Order_PP"
13:24:22Presenting theory "HOL-Algebra.Complete_Lattice"
13:24:24Presenting theory "Schoenhage_Strassen.FNTT_Rings"
13:24:24Presenting theory "Nullstellensatz.Univariate_PM"
13:24:24Presenting theory "HOL-Combinatorics.List_Permutation"
13:24:24Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
13:24:24Presenting theory "HOL-Analysis.Convex"
13:24:25Presenting theory "HOL-Algebra.Embedded_Algebras"
13:24:26Presenting theory "HOL-Algebra.Group"
13:24:26Presenting theory "HOL-Analysis.Finite_Cartesian_Product"
13:24:26Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
13:24:27Presenting theory "HOL-Algebra.FiniteProduct"
13:24:28Presenting theory "HOL-Algebra.Polynomial_Divisibility"
13:24:29Presenting theory "HOL-Algebra.Indexed_Polynomials"
13:24:30Presenting theory "HOL-Algebra.Finite_Extensions"
13:24:31Presenting theory "Nullstellensatz.Nullstellensatz"
13:24:31Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
13:24:31Presenting theory "HOL-Analysis.Cartesian_Space"
13:24:31Presenting theory "HOL-Algebra.Ring"
13:24:32Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:24:32Presenting theory "HOL-Algebra.Algebraic_Closure"
13:24:32Presenting theory "Groebner_Bases.Confluence"
13:24:32Presenting theory "HOL-Algebra.Divisibility"
13:24:32Presenting theory "HOL-Algebra.Algebraic_Closure_Type"
13:24:33Presenting theory "Jordan_Normal_Form.Missing_Ring"
13:24:33Presenting theory "Jordan_Normal_Form.Conjugate"
13:24:33Presenting theory "HOL-Algebra.Ideal_Product"
13:24:33Presenting theory "QHLProver.Complex_Matrix"
13:24:33Presenting file "$AFP/QHLProver/mat_alg.ML"
13:24:34Presenting theory "QHLProver.Gates"
13:24:34Presenting theory "HOL-Types_To_Sets.Prerequisites"
13:24:34Presenting theory "Nullstellensatz.Nullstellensatz_Field"
13:24:34Presenting theory "HOL-Algebra.Module"
13:24:34Presenting theory "HOL-Algebra.Chinese_Remainder"
13:24:34Presenting Signature_Groebner in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Signature_Groebner" ...
13:24:34Presenting document Signature_Groebner/document
13:24:34Presenting document Signature_Groebner/outline
13:24:34Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:24:34Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:24:34Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:24:34Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:24:34Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:24:34Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:24:35Presenting theory "HOL-Algebra.Generated_Rings"
13:24:35Presenting theory "HOL-Algebra.Generated_Fields"
13:24:35Presenting theory "HOL-Analysis.Determinants"
13:24:35Presenting theory "HOL-Types_To_Sets.Group_On_With"
13:24:35Presenting theory "Signature_Groebner.Prelims"
13:24:35Presenting theory "HOL-Algebra.QuotRing"
13:24:36Presenting theory "HOL-Algebra.Product_Groups"
13:24:36Presenting theory "HOL-Cardinals.Fun_More"
13:24:37Presenting theory "Signature_Groebner.More_MPoly"
13:24:38Presenting theory "HOL-Cardinals.Order_Relation_More"
13:24:38Presenting theory "Projective_Measurements.Linear_Algebra_Complements"
13:24:38Presenting theory "HOL-Cardinals.Wellfounded_More"
13:24:39Presenting theory "HOL-Algebra.Ring_Divisibility"
13:24:39Presenting theory "Groebner_Macaulay.Cone_Decomposition"
13:24:39Presenting theory "HOL-Cardinals.Wellorder_Relation"
13:24:39Presenting theory "HOL-Cardinals.Wellorder_Embedding"
13:24:40Presenting theory "HOL-Cardinals.Order_Union"
13:24:40Presenting theory "HOL-Algebra.Subrings"
13:24:40Presenting theory "HOL-Cardinals.Wellorder_Constructions"
13:24:41Presenting theory "Projective_Measurements.Projective_Measurements"
13:24:42Presenting theory "Groebner_Bases.Reduction"
13:24:42Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
13:24:43Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
13:24:43Presenting theory "HOL-Analysis.Abstract_Topology"
13:24:44Presenting theory "HOL-Algebra.Free_Abelian_Groups"
13:24:44Presenting theory "Projective_Measurements.CHSH_Inequality"
13:24:44Presenting theory "Jordan_Normal_Form.Matrix"
13:24:44Presenting HOL-Decision_Procs in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Decision_Procs" ...
13:24:44Presenting theory "HOL-Combinatorics.Cycles"
13:24:44Presenting theory "HOL-Analysis.FSigma"
13:24:44Presenting theory "HOL-Algebra.Solvable_Groups"
13:24:45Presenting theory "HOL-Analysis.Sum_Topology"
13:24:45Presenting theory "HOL-Algebra.Sym_Groups"
13:24:46Presenting theory "HOL-Algebra.Exact_Sequence"
13:24:46Presenting theory "HOL-Decision_Procs.Conversions"
13:24:46Presenting theory "HOL-Algebra.Left_Coset"
13:24:46Presenting theory "HOL-Algebra.SimpleGroups"
13:24:46Presenting theory "HOL-Algebra.SndIsomorphismGrp"
13:24:46Presenting theory "HOL-Algebra.Algebra"
13:24:46Presenting HOL-Quotient_Examples in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Quotient_Examples" ...
13:24:46Presenting theory "HOL-Decision_Procs.Algebra_Aux"
13:24:47Presenting theory "HOL-Algebra.Polynomials"
13:24:47Presenting theory "HOL-Quotient_Examples.DList"
13:24:48Presenting theory "Groebner_Macaulay.Dube_Bound"
13:24:48Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
13:24:49Presenting theory "HOL-Decision_Procs.Commutative_Ring"
13:24:49Presenting theory "HOL-Quotient_Examples.Quotient_FSet"
13:24:49Presenting theory "HOL-Analysis.Elementary_Topology"
13:24:49Presenting theory "HOL-Quotient_Examples.Quotient_Int"
13:24:49Presenting theory "Jordan_Normal_Form.Column_Operations"
13:24:50Presenting theory "HOL-Quotient_Examples.Quotient_Message"
13:24:50Presenting theory "HOL-Quotient_Examples.Lift_FSet"
13:24:50Presenting theory "HOL-Quotient_Examples.Lift_Set"
13:24:50Presenting theory "HOL-Analysis.Abstract_Limits"
13:24:50Presenting theory "HOL-Quotient_Examples.Lift_Fun"
13:24:50Presenting theory "HOL-Analysis.Continuum_Not_Denumerable"
13:24:51Presenting theory "HOL-Quotient_Examples.Quotient_Rat"
13:24:51Presenting theory "HOL-Quotient_Examples.Lift_DList"
13:24:51Presenting theory "Groebner_Bases.Groebner_Bases"
13:24:51Presenting theory "Groebner_Macaulay.Groebner_Macaulay_Examples"
13:24:51Presenting theory "HOL-Quotient_Examples.Int_Pow"
13:24:51Presenting Interpolation_Polynomials_HOL_Algebra in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Interpolation_Polynomials_HOL_Algebra" ...
13:24:51Presenting document Interpolation_Polynomials_HOL_Algebra/document
13:24:51Presenting document Interpolation_Polynomials_HOL_Algebra/outline
13:24:51Presenting theory "HOL-Algebra.Embedded_Algebras"
13:24:51Presenting theory "HOL-Quotient_Examples.Lifting_Code_Dt_Test"
13:24:51Presenting Jordan_Hoelder in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Jordan_Hoelder" ...
13:24:52Presenting document Jordan_Hoelder/document
13:24:52Presenting theory "Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials"
13:24:52Presenting document Jordan_Hoelder/outline
13:24:52Presenting theory "Jordan_Hoelder.MaximalNormalSubgroups"
13:24:52Presenting theory "Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation"
13:24:53Presenting theory "Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities"
13:24:53Presenting Jordan_Normal_Form in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Jordan_Normal_Form" ...
13:24:53Presenting document Jordan_Normal_Form/document
13:24:53Presenting document Jordan_Normal_Form/outline
13:24:54Presenting theory "HOL-Algebra.Polynomial_Divisibility"
13:24:54Presenting theory "Jordan_Normal_Form.Missing_Misc"
13:24:55Presenting theory "Secondary_Sylow.GroupAction"
13:24:55Presenting theory "Jordan_Normal_Form.Missing_Ring"
13:24:55Presenting theory "Finite_Fields.Finite_Fields_Preliminary_Results"
13:24:56Presenting theory "HOL-Analysis.Abstract_Topology_2"
13:24:56Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:24:56Presenting theory "Finite_Fields.Finite_Fields_Factorization_Ext"
13:24:56Presenting theory "Jordan_Normal_Form.Conjugate"
13:24:56Presenting theory "HOL-Algebra.IntRing"
13:24:57Presenting theory "Secondary_Sylow.SubgroupConjugation"
13:24:57Presenting theory "Finite_Fields.Ring_Characteristic"
13:24:57Presenting theory "Karatsuba.Abstract_Representations_2"
13:24:58Presenting theory "Schoenhage_Strassen.Z_mod_power_of_2"
13:24:58Presenting theory "Jordan_Normal_Form.Determinant"
13:24:58Presenting theory "Schoenhage_Strassen.Z_mod_power_of_2_TM"
13:24:58Presenting theory "HOL-Analysis.Connected"
13:24:59Presenting theory "Secondary_Sylow.SndSylow"
13:24:59Presenting theory "Schoenhage_Strassen.Z_mod_Fermat"
13:25:00Presenting theory "Schwartz_Zippel.Rand_Perfect_Matching"
13:25:00Presenting Isabelle_Marries_Dirac in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Isabelle_Marries_Dirac" ...
13:25:00Presenting document Isabelle_Marries_Dirac/document
13:25:00Presenting document Isabelle_Marries_Dirac/outline
13:25:00Presenting theory "Isabelle_Marries_Dirac.Basics"
13:25:00Presenting theory "Schoenhage_Strassen.Z_mod_Fermat_TM"
13:25:01Presenting theory "Signature_Groebner.Signature_Groebner"
13:25:01Presenting theory "Isabelle_Marries_Dirac.Binary_Nat"
13:25:01Presenting theory "Jordan_Hoelder.CompositionSeries"
13:25:02Presenting theory "Jordan_Hoelder.GroupIsoClasses"
13:25:02Presenting theory "HOL-Algebra.Weak_Morphisms"
13:25:02Presenting theory "HOL-Decision_Procs.Cooper"
13:25:02Presenting file "~~/src/HOL/Decision_Procs/cooper_tac.ML"
13:25:03Presenting theory "Signature_Groebner.Signature_Examples"
13:25:03Presenting theory "HOL-Algebra.Ideal_Product"
13:25:03Presenting theory "HOL-Analysis.Function_Topology"
13:25:03Presenting Linear_Programming in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Programming" ...
13:25:03Presenting document Linear_Programming/document
13:25:03Presenting document Linear_Programming/outline
13:25:03Presenting theory "Jordan_Hoelder.JordanHolder"
13:25:03Presenting Perron_Frobenius in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius" ...
13:25:03Presenting document Perron_Frobenius/document
13:25:03Presenting document Perron_Frobenius/outline
13:25:04Presenting theory "HOL-Analysis.L2_Norm"
13:25:04Presenting theory "Isabelle_Marries_Dirac.Quantum"
13:25:04Presenting theory "Linear_Programming.More_Jordan_Normal_Forms"
13:25:04Presenting theory "Simplex.Simplex_Algebra"
13:25:04Presenting theory "HOL-Analysis.Inner_Product"
13:25:04Presenting theory "Simplex.Abstract_Linear_Poly"
13:25:05Presenting theory "Jordan_Normal_Form.Matrix"
13:25:05Presenting theory "Simplex.Linear_Poly_Maps"
13:25:05Presenting theory "HOL-Analysis.Product_Vector"
13:25:05Presenting theory "Isabelle_Marries_Dirac.Complex_Vectors"
13:25:05Presenting theory "HOL-Algebra.Chinese_Remainder"
13:25:05Presenting theory "Simplex.QDelta"
13:25:05Presenting theory "HOL-Library.Type_Length"
13:25:05Presenting theory "Simplex.Simplex_Auxiliary"
13:25:05Presenting theory "HOL-Analysis.Euclidean_Space"
13:25:05Presenting theory "HOL-Analysis.Product_Topology"
13:25:05Presenting theory "Containers.Containers_Auxiliary"
13:25:06Presenting theory "Simplex.Rel_Chain"
13:25:06Presenting theory "Matrix.Utility"
13:25:07Presenting theory "Deriving.Generator_Aux"
13:25:07Presenting file "$AFP/Deriving/bnf_access.ML"
13:25:07Presenting file "$AFP/Deriving/generator_aux.ML"
13:25:07Presenting theory "Deriving.Derive_Manager"
13:25:07Presenting file "$AFP/Deriving/derive_manager.ML"
13:25:07Presenting theory "HOL-Analysis.Linear_Algebra"
13:25:08Presenting theory "HOL-Analysis.T1_Spaces"
13:25:08Presenting theory "Containers.Containers_Generator"
13:25:08Presenting file "$AFP/Containers/containers_generator.ML"
13:25:08Presenting theory "HOL-Analysis.Lindelof_Spaces"
13:25:09Presenting theory "HOL-Analysis.Metric_Arith"
13:25:09Presenting file "~~/src/HOL/Analysis/metric_arith.ML"
13:25:09Presenting theory "Containers.Collection_Enum"
13:25:09Presenting file "$AFP/Containers/cenum_generator.ML"
13:25:11Presenting theory "HOL-Analysis.Affine"
13:25:11Presenting theory "Matrix.Matrix_Legacy"
13:25:12Presenting theory "Deriving.Equality_Generator"
13:25:12Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
13:25:12Presenting theory "HOL-Decision_Procs.Dense_Linear_Order"
13:25:12Presenting theory "Deriving.Equality_Instances"
13:25:12Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML"
13:25:12Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML"
13:25:12Presenting file "~~/src/HOL/Decision_Procs/langford.ML"
13:25:12Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"
13:25:12Presenting theory "HOL-Decision_Procs.DP_Library"
13:25:13Presenting theory "Containers.Collection_Eq"
13:25:13Presenting file "$AFP/Containers/ceq_generator.ML"
13:25:13Presenting theory "Containers.Equal"
13:25:13Presenting theory "Containers.DList_Set"
13:25:14Presenting theory "Containers.List_Fusion"
13:25:15Presenting theory "Containers.Lexicographic_Order"
13:25:15Presenting theory "Containers.Extend_Partial_Order"
13:25:17Presenting theory "HOL-Library.Word"
13:25:17Presenting theory "HOL-Analysis.Convex"
13:25:17Presenting theory "Simplex.Simplex"
13:25:17Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
13:25:17Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
13:25:18Presenting theory "Word_Lib.Bit_Comprehension"
13:25:18Presenting theory "HOL-Analysis.Elementary_Metric_Spaces"
13:25:18Presenting theory "Karatsuba.Int_LSBF"
13:25:18Presenting theory "Containers.Set_Linorder"
13:25:19Presenting theory "Deriving.Comparator"
13:25:20Presenting theory "Karatsuba.Karatsuba"
13:25:20Presenting theory "Deriving.Comparator_Generator"
13:25:20Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
13:25:20Presenting theory "Farkas.Farkas"
13:25:20Presenting theory "Deriving.Compare"
13:25:20Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
13:25:21Presenting theory "Deriving.Compare_Generator"
13:25:21Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
13:25:21Presenting theory "Deriving.Compare_Instances"
13:25:21Presenting theory "Containers.Collection_Order"
13:25:21Presenting file "$AFP/Containers/ccompare_generator.ML"
13:25:22Presenting theory "Containers.RBT_ext"
13:25:23Presenting theory "Deriving.RBT_Comparator_Impl"
13:25:23Presenting theory "Simplex.Simplex_Incremental"
13:25:23Presenting theory "HOL-Analysis.Elementary_Topology"
13:25:23Presenting theory "Farkas.Simplex_for_Reals"
13:25:23Presenting theory "Containers.RBT_Mapping2"
13:25:23Presenting theory "Farkas.Matrix_Farkas"
13:25:24Presenting theory "HOL-Analysis.Elementary_Normed_Spaces"
13:25:24Presenting theory "Containers.RBT_Set2"
13:25:24Presenting theory "Containers.Closure_Set"
13:25:24Presenting theory "Linear_Programming.Matrix_LinPoly"
13:25:25Presenting theory "HOL-Decision_Procs.Ferrack"
13:25:25Presenting file "~~/src/HOL/Decision_Procs/ferrack_tac.ML"
13:25:25Presenting theory "HOL-Analysis.Norm_Arith"
13:25:26Presenting file "~~/src/HOL/Analysis/normarith.ML"
13:25:27Presenting theory "Linear_Programming.LP_Preliminaries"
13:25:28Presenting theory "Linear_Programming.Linear_Programming"
13:25:28Presenting QHLProver in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QHLProver" ...
13:25:28Presenting document QHLProver/document
13:25:28Presenting document QHLProver/outline
13:25:29Presenting theory "Schoenhage_Strassen.Schoenhage_Strassen"
13:25:30Presenting theory "Karatsuba.Karatsuba_TM"
13:25:31Presenting theory "HOL-Analysis.Topology_Euclidean_Space"
13:25:31Presenting theory "Matrix_Tensor.Matrix_Tensor"
13:25:32Presenting theory "Schoenhage_Strassen.Schoenhage_Strassen_TM"
13:25:32Presenting Uncertainty_Principle in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Uncertainty_Principle" ...
13:25:32Presenting document Uncertainty_Principle/document
13:25:32Presenting document Uncertainty_Principle/outline
13:25:33Presenting theory "Uncertainty_Principle.Uncertainty_Principle"
13:25:33Presenting Subresultants in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Subresultants" ...
13:25:33Presenting document Subresultants/document
13:25:33Presenting document Subresultants/outline
13:25:33Presenting theory "Subresultants.Resultant_Prelim"
13:25:33Presenting theory "Subresultants.Dichotomous_Lazard"
13:25:33Presenting theory "Subresultants.Binary_Exponentiation"
13:25:33Presenting theory "Subresultants.More_Homomorphisms"
13:25:33Presenting theory "Subresultants.Coeff_Int"
13:25:33Presenting theory "HOL-Analysis.Line_Segment"
13:25:34Presenting theory "Isabelle_Marries_Dirac.Tensor"
13:25:34Presenting theory "Containers.Set_Impl"
13:25:34Presenting file "$AFP/Containers/set_impl_generator.ML"
13:25:34Presenting theory "Jordan_Normal_Form.Matrix_IArray_Impl"
13:25:35Presenting theory "HOL-Analysis.Abstract_Topology"
13:25:36Presenting theory "HOL-Analysis.Continuum_Not_Denumerable"
13:25:36Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:25:36Presenting theory "Isabelle_Marries_Dirac.More_Tensor"
13:25:37Presenting theory "QHLProver.Complex_Matrix"
13:25:37Presenting file "$AFP/QHLProver/mat_alg.ML"
13:25:38Presenting theory "HOL-Analysis.Abstract_Topology_2"
13:25:38Presenting theory "Groebner_Bases.Algorithm_Schema"
13:25:38Presenting theory "HOL-Analysis.Metric_Arith"
13:25:38Presenting file "~~/src/HOL/Analysis/metric_arith.ML"
13:25:39Presenting theory "Isabelle_Marries_Dirac.Measurement"
13:25:40Presenting theory "Isabelle_Marries_Dirac.Entanglement"
13:25:40Presenting theory "HOL-Analysis.Convex_Euclidean_Space"
13:25:40Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
13:25:41Presenting theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl"
13:25:41Presenting theory "Groebner_Bases.Buchberger"
13:25:41Presenting theory "Polynomials.PP_Type"
13:25:41Presenting theory "Deriving.Comparator"
13:25:42Presenting theory "Subresultants.Subresultant"
13:25:42Presenting theory "Isabelle_Marries_Dirac.Quantum_Teleportation"
13:25:43Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:25:43Presenting theory "QHLProver.Matrix_Limit"
13:25:44Presenting theory "Isabelle_Marries_Dirac.Deutsch"
13:25:44Presenting theory "Polynomial_Factorization.Missing_Polynomial_Factorial"
13:25:44Presenting theory "Jordan_Normal_Form.Column_Operations"
13:25:45Presenting theory "Subresultants.Subresultant_Gcd"
13:25:45Presenting Berlekamp_Zassenhaus in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Berlekamp_Zassenhaus" ...
13:25:45Presenting document Berlekamp_Zassenhaus/document
13:25:45Presenting document Berlekamp_Zassenhaus/outline
13:25:46Presenting theory "HOL-Analysis.Elementary_Metric_Spaces"
13:25:46Presenting theory "Polynomials.OAlist"
13:25:47Presenting theory "QHLProver.Quantum_Program"
13:25:47Presenting theory "HOL-Number_Theory.Cong"
13:25:47Presenting theory "Deep_Learning.Tensor"
13:25:47Presenting theory "Polynomials.OAlist_Poly_Mapping"
13:25:47Presenting theory "Deep_Learning.Tensor_Subtensor"
13:25:48Presenting theory "Deep_Learning.Tensor_Plus"
13:25:48Presenting theory "Deep_Learning.Tensor_Matricization"
13:25:49Presenting theory "HOL-Number_Theory.Totient"
13:25:49Presenting theory "Polynomials.Term_Order"
13:25:49Presenting theory "Isabelle_Marries_Dirac.Deutsch_Jozsa"
13:25:50Presenting theory "HOL-Analysis.Finite_Cartesian_Product"
13:25:50Presenting theory "QHLProver.Partial_State"
13:25:50Presenting theory "HOL-Number_Theory.Residues"
13:25:50Presenting theory "Polynomials.MPoly_Type_Class_OAlist"
13:25:51Presenting theory "Groebner_Bases.Benchmarks"
13:25:51Presenting theory "Groebner_Bases.Algorithm_Schema_Impl"
13:25:51Presenting theory "QHLProver.Gates"
13:25:51Presenting theory "Groebner_Bases.Code_Target_Rat"
13:25:51Presenting theory "Isabelle_Marries_Dirac.No_Cloning"
13:25:51Presenting theory "Berlekamp_Zassenhaus.Finite_Field"
13:25:51Presenting theory "Groebner_Bases.Buchberger_Examples"
13:25:52Presenting theory "Groebner_Bases.More_MPoly_Type_Class"
13:25:52Presenting theory "Berlekamp_Zassenhaus.Arithmetic_Record_Based"
13:25:53Presenting theory "Word_Lib.More_Arithmetic"
13:25:53Presenting theory "Jordan_Normal_Form.Determinant"
13:25:53Presenting theory "QHLProver.Quantum_Hoare"
13:25:53Presenting theory "Word_Lib.More_Divides"
13:25:54Presenting theory "Groebner_Bases.Auto_Reduction"
13:25:54Presenting theory "Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma"
13:25:54Presenting theory "Word_Lib.More_Bit_Ring"
13:25:54Presenting theory "HOL-Analysis.Cartesian_Space"
13:25:54Presenting Algebraic_Numbers in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Algebraic_Numbers" ...
13:25:54Presenting document Algebraic_Numbers/document
13:25:54Presenting document Algebraic_Numbers/outline
13:25:54Presenting theory "Deriving.Compare_Rat"
13:25:54Presenting theory "Deriving.Compare_Real"
13:25:55Presenting theory "Groebner_Bases.Reduced_GB"
13:25:55Presenting theory "Groebner_Bases.Reduced_GB_Examples"
13:25:56Presenting theory "QHLProver.Grover"
13:25:56Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:25:56Presenting theory "HOL-Analysis.Connected"
13:25:56Presenting theory "Algebraic_Numbers.Algebraic_Numbers_Prelim"
13:25:56Presenting theory "Jordan_Normal_Form.Determinant_Impl"
13:25:56Presenting theory "Jordan_Normal_Form.Missing_Misc"
13:25:56Presenting BenOr_Kozen_Reif in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/BenOr_Kozen_Reif" ...
13:25:57Presenting document BenOr_Kozen_Reif/document
13:25:57Presenting document BenOr_Kozen_Reif/outline
13:25:57Presenting theory "Sturm_Tarski.PolyMisc"
13:25:57Presenting theory "Jordan_Normal_Form.Missing_Ring"
13:25:58Presenting theory "Jordan_Normal_Form.Conjugate"
13:25:58Presenting theory "HOL-Analysis.Starlike"
13:25:58Presenting theory "Algebraic_Numbers.Bivariate_Polynomials"
13:25:59Presenting theory "Word_Lib.More_Word"
13:25:59Presenting theory "Sturm_Tarski.Sturm_Tarski"
13:25:59Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
13:26:00Presenting theory "Word_Lib.Most_significant_bit"
13:26:00Presenting theory "HOL-Analysis.Elementary_Normed_Spaces"
13:26:00Presenting theory "Word_Lib.Least_significant_bit"
13:26:00Presenting theory "Show.Show"
13:26:00Presenting file "$AFP/Show/show_generator.ML"
13:26:00Presenting theory "Jordan_Normal_Form.Show_Matrix"
13:26:00Presenting theory "Word_Lib.Generic_set_bit"
13:26:00Presenting theory "Word_Lib.Bit_Comprehension"
13:26:00Presenting theory "Word_Lib.Signed_Division_Word"
13:26:00Presenting theory "Algebraic_Numbers.Resultant"
13:26:01Presenting theory "Native_Word.Code_Target_Word_Base"
13:26:01Presenting theory "Show.Show_Instances"
13:26:01Presenting theory "Native_Word.Word_Type_Copies"
13:26:01Presenting theory "Jordan_Normal_Form.Matrix"
13:26:01Presenting theory "Native_Word.Code_Int_Integer_Conversion"
13:26:02Presenting theory "Show.Shows_Literal"
13:26:02Presenting theory "Jordan_Normal_Form.Shows_Literal_Matrix"
13:26:02Presenting theory "BenOr_Kozen_Reif.More_Matrix"
13:26:02Presenting theory "HOL-Analysis.Norm_Arith"
13:26:02Presenting theory "Native_Word.Code_Target_Integer_Bit"
13:26:02Presenting file "~~/src/HOL/Analysis/normarith.ML"
13:26:02Presenting theory "Polynomial_Factorization.Order_Polynomial"
13:26:02Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
13:26:03Presenting theory "Native_Word.Uint32"
13:26:03Presenting theory "BenOr_Kozen_Reif.BKR_Algorithm"
13:26:03Presenting theory "HOL-Decision_Procs.MIR"
13:26:03Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:26:03Presenting theory "Native_Word.Uint64"
13:26:04Presenting theory "Native_Word.Code_Target_Int_Bit"
13:26:04Presenting theory "Algebraic_Numbers.Algebraic_Numbers"
13:26:04Presenting file "~~/src/HOL/Decision_Procs/mir_tac.ML"
13:26:04Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
13:26:04Presenting theory "Pure-ex.Guess"
13:26:05Presenting theory "Jordan_Normal_Form.Char_Poly"
13:26:05Presenting theory "BenOr_Kozen_Reif.Matrix_Equation_Construction"
13:26:06Presenting theory "Groebner_Bases.Macaulay_Matrix"
13:26:06Presenting theory "Berlekamp_Zassenhaus.Finite_Field_Record_Based"
13:26:06Presenting theory "HOL-Analysis.Topology_Euclidean_Space"
13:26:06Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form"
13:26:06Presenting theory "HOL-Analysis.Path_Connected"
13:26:07Presenting theory "VectorSpace.RingModuleFacts"
13:26:07Presenting theory "VectorSpace.FunctionLemmas"
13:26:07Presenting theory "Sturm_Sequences.Misc_Polynomial"
13:26:07Presenting theory "VectorSpace.MonoidSums"
13:26:07Presenting theory "Sturm_Sequences.Sturm_Library"
13:26:08Presenting theory "VectorSpace.LinearCombinations"
13:26:08Presenting theory "Berlekamp_Zassenhaus.Matrix_Record_Based"
13:26:09Presenting theory "VectorSpace.SumSpaces"
13:26:09Presenting theory "Matrix.Utility"
13:26:09Presenting theory "Polynomial_Factorization.Polynomial_Irreducibility"
13:26:09Presenting theory "HOL-Analysis.Line_Segment"
13:26:10Presenting theory "VectorSpace.VectorSpace"
13:26:10Presenting theory "HOL-Analysis.Locally"
13:26:10Presenting theory "HOL-Analysis.Uncountable_Sets"
13:26:11Presenting theory "Jordan_Normal_Form.Missing_VectorSpace"
13:26:12Presenting theory "Groebner_Bases.F4"
13:26:13Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:26:13Presenting theory "Sturm_Sequences.Sturm_Theorem"
13:26:13Presenting theory "Containers.Containers_Auxiliary"
13:26:13Presenting theory "HOL-Analysis.Convex_Euclidean_Space"
13:26:13Presenting theory "Deriving.Generator_Aux"
13:26:13Presenting file "$AFP/Deriving/bnf_access.ML"
13:26:13Presenting file "$AFP/Deriving/generator_aux.ML"
13:26:14Presenting theory "Deriving.Derive_Manager"
13:26:14Presenting file "$AFP/Deriving/derive_manager.ML"
13:26:14Presenting theory "BenOr_Kozen_Reif.BKR_Proofs"
13:26:14Presenting theory "Containers.Containers_Generator"
13:26:14Presenting file "$AFP/Containers/containers_generator.ML"
13:26:14Presenting theory "Jordan_Normal_Form.VS_Connect"
13:26:14Presenting theory "Algebraic_Numbers.Sturm_Rat"
13:26:14Presenting theory "Containers.Collection_Enum"
13:26:14Presenting file "$AFP/Containers/cenum_generator.ML"
13:26:15Presenting theory "Deriving.Equality_Generator"
13:26:15Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
13:26:15Presenting theory "Deriving.Equality_Instances"
13:26:15Presenting theory "Polynomial_Factorization.Square_Free_Factorization"
13:26:15Presenting theory "Containers.Collection_Eq"
13:26:15Presenting theory "Jordan_Normal_Form.Gram_Schmidt"
13:26:15Presenting file "$AFP/Containers/ceq_generator.ML"
13:26:15Presenting theory "Containers.Equal"
13:26:15Presenting theory "Algebraic_Numbers.Factors_of_Int_Poly"
13:26:15Presenting theory "Containers.DList_Set"
13:26:16Presenting theory "Algebraic_Numbers.Min_Int_Poly"
13:26:16Presenting theory "Containers.List_Fusion"
13:26:16Presenting theory "Containers.Lexicographic_Order"
13:26:16Presenting theory "Containers.Extend_Partial_Order"
13:26:17Presenting theory "Jordan_Normal_Form.Schur_Decomposition"
13:26:17Presenting theory "HOL-Decision_Procs.Approximation_Bounds"
13:26:17Presenting theory "Algebraic_Numbers.Algebraic_Numbers_Pre_Impl"
13:26:17Presenting theory "Algebraic_Numbers.Cauchy_Root_Bound"
13:26:19Presenting theory "Containers.Set_Linorder"
13:26:19Presenting theory "BenOr_Kozen_Reif.BKR_Decision"
13:26:20Presenting theory "Deriving.Comparator_Generator"
13:26:20Presenting theory "BenOr_Kozen_Reif.Renegar_Algorithm"
13:26:20Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
13:26:20Presenting theory "Deriving.Compare"
13:26:20Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
13:26:20Presenting theory "Polynomial_Factorization.Missing_List"
13:26:21Presenting theory "Deriving.Compare_Generator"
13:26:21Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
13:26:21Presenting theory "Deriving.Compare_Instances"
13:26:21Presenting theory "Polynomial_Factorization.Missing_Multiset"
13:26:21Presenting theory "Containers.Collection_Order"
13:26:21Presenting file "$AFP/Containers/ccompare_generator.ML"
13:26:22Presenting theory "Berlekamp_Zassenhaus.More_Missing_Multiset"
13:26:22Presenting theory "Containers.RBT_ext"
13:26:23Presenting theory "Deriving.RBT_Comparator_Impl"
13:26:23Presenting theory "Containers.RBT_Mapping2"
13:26:23Presenting theory "Berlekamp_Zassenhaus.Unique_Factorization"
13:26:23Presenting theory "Containers.RBT_Set2"
13:26:23Presenting theory "Containers.Closure_Set"
13:26:26Presenting theory "Berlekamp_Zassenhaus.Unique_Factorization_Poly"
13:26:27Presenting theory "HOL-Analysis.Starlike"
13:26:27Presenting theory "Algebraic_Numbers.Real_Algebraic_Numbers"
13:26:27Presenting theory "Berlekamp_Zassenhaus.Poly_Mod"
13:26:28Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
13:26:28Presenting theory "HOL-Analysis.Homotopy"
13:26:28Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:26:28Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:26:28Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:26:28Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:26:28Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:26:28Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:26:28Presenting theory "HOL-Decision_Procs.Approximation"
13:26:28Presenting theory "Containers.Set_Impl"
13:26:28Presenting file "~~/src/HOL/Decision_Procs/approximation.ML"
13:26:28Presenting file "~~/src/HOL/Decision_Procs/approximation_generator.ML"
13:26:28Presenting file "$AFP/Containers/set_impl_generator.ML"
13:26:28Presenting theory "Berlekamp_Zassenhaus.Poly_Mod_Finite_Field"
13:26:29Presenting theory "Jordan_Normal_Form.Matrix_Impl"
13:26:29Presenting theory "Berlekamp_Zassenhaus.Karatsuba_Multiplication"
13:26:29Presenting theory "Jordan_Normal_Form.Matrix_IArray_Impl"
13:26:29Presenting theory "HOL-Analysis.Abstract_Limits"
13:26:29Presenting theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl"
13:26:29Presenting theory "Algebraic_Numbers.Real_Roots"
13:26:29Presenting theory "Berlekamp_Zassenhaus.Polynomial_Record_Based"
13:26:30Presenting theory "Jordan_Normal_Form.Strassen_Algorithm"
13:26:30Presenting theory "HOL-Decision_Procs.Rat_Pair"
13:26:30Presenting theory "Jordan_Normal_Form.Strassen_Algorithm_Code"
13:26:30Presenting theory "Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based"
13:26:30Presenting theory "BenOr_Kozen_Reif.Renegar_Proofs"
13:26:30Presenting theory "Berlekamp_Zassenhaus.Chinese_Remainder_Poly"
13:26:30Presenting theory "HOL-Analysis.Abstract_Euclidean_Space"
13:26:30Presenting theory "Groebner_Bases.F4_Examples"
13:26:31Presenting theory "Algebraic_Numbers.Complex_Roots_Real_Poly"
13:26:31Presenting theory "Algebraic_Numbers.Compare_Complex"
13:26:31Presenting theory "BenOr_Kozen_Reif.Renegar_Decision"
13:26:31Presenting theory "Regular-Sets.Regular_Set"
13:26:31Presenting Cubic_Quartic_Equations in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cubic_Quartic_Equations" ...
13:26:31Presenting document Cubic_Quartic_Equations/document
13:26:31Presenting document Cubic_Quartic_Equations/outline
13:26:31Presenting theory "Complex_Geometry.More_Transcendental"
13:26:32Presenting theory "Complex_Geometry.Canonical_Angle"
13:26:32Presenting theory "Regular-Sets.Regular_Exp"
13:26:32Presenting theory "HOL-Decision_Procs.Polynomial_List"
13:26:32Presenting theory "Complex_Geometry.More_Complex"
13:26:32Presenting theory "Algebraic_Numbers.Interval_Arithmetic"
13:26:32Presenting theory "Cubic_Quartic_Equations.Ferraris_Formula"
13:26:32Presenting theory "Regular-Sets.NDerivative"
13:26:33Presenting theory "Cubic_Quartic_Equations.Cardanos_Formula"
13:26:33Presenting theory "Factor_Algebraic_Polynomial.Roots_via_IA"
13:26:33Presenting theory "Regular-Sets.Equivalence_Checking"
13:26:34Presenting theory "Regular-Sets.Relation_Interpretation"
13:26:34Presenting theory "Cubic_Quartic_Equations.Complex_Roots"
13:26:34Presenting theory "Regular-Sets.Regexp_Method"
13:26:34Presenting theory "Cubic_Quartic_Equations.Cubic_Polynomials"
13:26:34Presenting theory "Cubic_Quartic_Equations.Quartic_Polynomials"
13:26:34Presenting Factor_Algebraic_Polynomial in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factor_Algebraic_Polynomial" ...
13:26:34Presenting document Factor_Algebraic_Polynomial/document
13:26:34Presenting document Factor_Algebraic_Polynomial/outline
13:26:35Presenting theory "HOL-Analysis.Function_Topology"
13:26:35Presenting theory "Polynomials.MPoly_Type"
13:26:35Presenting theory "HOL-Decision_Procs.Reflected_Multivariate_Polynomial"
13:26:35Presenting theory "Abstract-Rewriting.Seq"
13:26:35Presenting theory "Berlekamp_Zassenhaus.Berlekamp_Type_Based"
13:26:36Presenting theory "Algebraic_Numbers.Complex_Algebraic_Numbers"
13:26:36Presenting theory "Polynomials.More_MPoly_Type"
13:26:36Presenting theory "Show.Show_Real"
13:26:36Presenting theory "Polynomials.MPoly_Type_Univariate"
13:26:36Presenting theory "Algebraic_Numbers.Show_Real_Alg"
13:26:36Presenting theory "Algebraic_Numbers.Show_Real_Approx"
13:26:36Presenting theory "Groebner_Bases.Syzygy"
13:26:36Presenting theory "Symmetric_Polynomials.Vieta"
13:26:36Presenting theory "HOL-Analysis.Product_Topology"
13:26:37Presenting theory "Algebraic_Numbers.Show_Real_Precise"
13:26:37Presenting theory "Show.Show_Complex"
13:26:37Presenting theory "Algebraic_Numbers.Algebraic_Number_Tests"
13:26:37Presenting theory "Algebraic_Numbers.Algebraic_Numbers_External_Code"
13:26:37Presenting Quantifier_Elimination_Hybrid in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quantifier_Elimination_Hybrid" ...
13:26:37Presenting document Quantifier_Elimination_Hybrid/document
13:26:37Presenting document Quantifier_Elimination_Hybrid/outline
13:26:39Presenting theory "Polynomials.MPoly_Type"
13:26:39Presenting theory "HOL-Decision_Procs.Parametric_Ferrante_Rackoff"
13:26:40Presenting theory "HOL-Analysis.T1_Spaces"
13:26:40Presenting theory "Berlekamp_Zassenhaus.Distinct_Degree_Factorization"
13:26:40Presenting theory "HOL-Decision_Procs.Commutative_Ring_Complete"
13:26:40Presenting theory "Berlekamp_Zassenhaus.Finite_Field_Factorization"
13:26:40Presenting theory "Groebner_Bases.Syzygy_Examples"
13:26:40Presenting theory "Polynomial_Interpolation.Improved_Code_Equations"
13:26:41Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
13:26:41Presenting theory "Polynomials.More_MPoly_Type"
13:26:41Presenting theory "HOL-Decision_Procs.Reflective_Field"
13:26:41Presenting theory "Polynomials.Quasi_PM_Power_Products"
13:26:41Presenting theory "HOL-Decision_Procs.Commutative_Ring_Ex"
13:26:41Presenting theory "HOL-Decision_Procs.Approximation_Ex"
13:26:41Presenting theory "HOL-Decision_Procs.Approximation_Quickcheck_Ex"
13:26:41Presenting theory "HOL-Decision_Procs.Dense_Linear_Order_Ex"
13:26:41Presenting theory "HOL-Decision_Procs.Decision_Procs"
13:26:41Presenting CRYSTALS-Kyber in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CRYSTALS-Kyber" ...
13:26:42Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
13:26:42Presenting document CRYSTALS-Kyber/document
13:26:42Presenting document CRYSTALS-Kyber/outline
13:26:42Presenting theory "Polynomials.MPoly_Type_Univariate"
13:26:42Presenting theory "CRYSTALS-Kyber.Kyber_spec"
13:26:42Presenting theory "Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based"
13:26:42Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
13:26:42Presenting theory "CRYSTALS-Kyber.Mod_Plus_Minus"
13:26:42Presenting theory "Well_Quasi_Orders.Least_Enum"
13:26:42Presenting theory "Symmetric_Polynomials.Vieta"
13:26:42Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
13:26:42Presenting theory "CRYSTALS-Kyber.Abs_Qr"
13:26:42Presenting theory "HOL-Analysis.L2_Norm"
13:26:43Presenting theory "Open_Induction.Restricted_Predicates"
13:26:43Presenting theory "HOL-Analysis.Inner_Product"
13:26:43Presenting theory "Well_Quasi_Orders.Almost_Full"
13:26:44Presenting theory "Well_Quasi_Orders.Minimal_Elements"
13:26:44Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
13:26:45Presenting theory "HOL-Analysis.Product_Vector"
13:26:45Presenting theory "HOL-Analysis.Path_Connected"
13:26:45Presenting theory "HOL-Analysis.Euclidean_Space"
13:26:45Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
13:26:46Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
13:26:46Presenting theory "HOL-Analysis.Abstract_Topological_Spaces"
13:26:46Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
13:26:46Presenting theory "HOL-Analysis.Uncountable_Sets"
13:26:46Presenting theory "Abstract-Rewriting.SN_Orders"
13:26:46Presenting theory "HOL-Analysis.Finite_Cartesian_Product"
13:26:46Presenting theory "Polynomials.Utils"
13:26:47Presenting theory "Matrix.Ordered_Semiring"
13:26:47Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
13:26:47Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
13:26:47Presenting theory "Well_Quasi_Orders.Least_Enum"
13:26:47Presenting theory "CRYSTALS-Kyber.Compress"
13:26:47Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
13:26:48Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
13:26:48Presenting theory "Open_Induction.Restricted_Predicates"
13:26:48Presenting theory "CRYSTALS-Kyber.Crypto_Scheme"
13:26:48Presenting theory "Berlekamp_Zassenhaus.Hensel_Lifting"
13:26:48Presenting theory "CRYSTALS-Kyber.Kyber_Values"
13:26:48Presenting theory "CRYSTALS-Kyber.Mod_Ring_Numeral"
13:26:48Presenting theory "HOL-Number_Theory.Fib"
13:26:49Presenting theory "HOL-Number_Theory.Eratosthenes"
13:26:49Presenting theory "HOL-Number_Theory.Mod_Exp"
13:26:49Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:26:49Presenting theory "HOL-Number_Theory.Gauss"
13:26:49Presenting theory "Jordan_Normal_Form.Matrix_Comparison"
13:26:50Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:26:50Presenting theory "Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based"
13:26:50Presenting theory "Well_Quasi_Orders.Almost_Full"
13:26:51Presenting theory "Abstract-Rewriting.SN_Order_Carrier"
13:26:51Presenting theory "Jordan_Normal_Form.Ring_Hom_Matrix"
13:26:51Presenting theory "Jordan_Normal_Form.Derivation_Bound"
13:26:51Presenting theory "Jordan_Normal_Form.Complexity_Carrier"
13:26:51Presenting theory "Well_Quasi_Orders.Minimal_Elements"
13:26:51Presenting theory "Jordan_Normal_Form.Show_Arctic"
13:26:51Presenting theory "Berlekamp_Zassenhaus.Berlekamp_Hensel"
13:26:52Presenting theory "Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary"
13:26:52Presenting theory "Jordan_Normal_Form.Matrix_Complexity"
13:26:52Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
13:26:52Presenting theory "HOL-Number_Theory.Pocklington"
13:26:52Presenting theory "Sqrt_Babylonian.Log_Impl"
13:26:53Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
13:26:54Presenting theory "HOL-Number_Theory.Prime_Powers"
13:26:54Presenting theory "HOL-Analysis.Abstract_Metric_Spaces"
13:26:54Presenting theory "Cauchy.CauchysMeanTheorem"
13:26:55Presenting theory "Polynomials.Utils"
13:26:55Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
13:26:56Presenting theory "Polynomials.Power_Products"
13:26:56Presenting theory "Polynomials.MPoly_PM"
13:26:56Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:26:56Presenting theory "Jordan_Normal_Form.Matrix_Kernel"
13:26:56Presenting theory "HOL-Number_Theory.Number_Theory"
13:26:57Presenting theory "Sqrt_Babylonian.NthRoot_Impl"
13:26:57Presenting theory "Groebner_Bases.Groebner_PM"
13:26:57Presenting theory "Number_Theoretic_Transform.Preliminary_Lemmas"
13:26:57Presenting CVP_Hardness in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CVP_Hardness" ...
13:26:57Presenting document CVP_Hardness/document
13:26:57Presenting document CVP_Hardness/outline
13:26:57Presenting theory "CVP_Hardness.Reduction"
13:26:57Presenting theory "Polynomials.More_Modules"
13:26:58Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness"
13:26:58Presenting theory "Sqrt_Babylonian.Sqrt_Babylonian"
13:26:58Presenting theory "Polynomial_Factorization.Explicit_Roots"
13:26:58Presenting theory "Number_Theoretic_Transform.NTT"
13:26:58Presenting theory "Jordan_Normal_Form.Spectral_Radius"
13:26:59Presenting theory "Polynomial_Interpolation.Divmod_Int"
13:26:59Presenting theory "Jordan_Normal_Form.DL_Missing_List"
13:26:59Presenting theory "Polynomial_Interpolation.Is_Rat_To_Rat"
13:26:59Presenting theory "HOL-Analysis.Infinite_Sum"
13:26:59Presenting theory "BenOr_Kozen_Reif.More_Matrix"
13:27:00Presenting theory "HOL-Analysis.Ordered_Euclidean_Space"
13:27:01Presenting theory "CVP_Hardness.Lattice_int"
13:27:01Presenting theory "Jordan_Normal_Form.DL_Rank"
13:27:01Presenting theory "CVP_Hardness.Partition"
13:27:01Presenting theory "CVP_Hardness.Subset_Sum"
13:27:01Presenting theory "CVP_Hardness.CVP_p"
13:27:02Presenting theory "Algebraic_Numbers.Bivariate_Polynomials"
13:27:02Presenting theory "CRYSTALS-Kyber.NTT_Scheme"
13:27:03Presenting theory "HOL-Analysis.Arcwise_Connected"
13:27:03Presenting theory "CRYSTALS-Kyber.Crypto_Scheme_NTT"
13:27:03Presenting theory "Polynomial_Interpolation.Newton_Interpolation"
13:27:03Presenting theory "CRYSTALS-Kyber.Powers3844"
13:27:03Presenting theory "CRYSTALS-Kyber.Kyber_NTT_Values"
13:27:03Presenting Fishers_Inequality in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fishers_Inequality" ...
13:27:03Presenting document Fishers_Inequality/document
13:27:03Presenting document Fishers_Inequality/outline
13:27:03Presenting theory "Algebraic_Numbers.Resultant"
13:27:03Presenting theory "Polynomial_Interpolation.Lagrange_Interpolation"
13:27:04Presenting theory "Jordan_Normal_Form.DL_Missing_Sublist"
13:27:04Presenting theory "Polynomials.MPoly_Type_Class"
13:27:04Presenting theory "LLL_Basis_Reduction.Missing_Lemmas"
13:27:04Presenting theory "Jordan_Normal_Form.DL_Submatrix"
13:27:04Presenting theory "Polynomial_Interpolation.Neville_Aitken_Interpolation"
13:27:04Presenting theory "Card_Partitions.Set_Partition"
13:27:05Presenting theory "LLL_Basis_Reduction.Norms"
13:27:05Presenting theory "CVP_Hardness.infnorm"
13:27:05Presenting theory "Polynomial_Interpolation.Polynomial_Interpolation"
13:27:05Presenting theory "CVP_Hardness.CVP_vec"
13:27:05Presenting theory "Jordan_Normal_Form.DL_Rank_Submatrix"
13:27:05Presenting LLL_Basis_Reduction in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction" ...
13:27:05Presenting theory "CVP_Hardness.Digits_int"
13:27:05Presenting document LLL_Basis_Reduction/document
13:27:05Presenting document LLL_Basis_Reduction/outline
13:27:06Presenting theory "Polynomials.Power_Products"
13:27:06Presenting theory "CVP_Hardness.Additional_Lemmas"
13:27:07Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
13:27:07Presenting theory "Nested_Multisets_Ordinals.Multiset_More"
13:27:07Presenting theory "HOL-Analysis.Homotopy"
13:27:07Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide"
13:27:07Presenting theory "Nested_Multisets_Ordinals.Duplicate_Free_Multiset"
13:27:08Presenting theory "Polynomial_Factorization.Prime_Factorization"
13:27:08Presenting theory "Polynomials.More_Modules"
13:27:08Presenting theory "Algebraic_Numbers.Bivariate_Polynomials"
13:27:08Presenting theory "Polynomial_Factorization.Precomputation"
13:27:08Presenting theory "CVP_Hardness.BHLE"
13:27:09Presenting theory "Polynomial_Factorization.Gauss_Lemma"
13:27:09Presenting theory "CVP_Hardness.SVP_vec"
13:27:09Presenting LLL_Factorization in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization" ...
13:27:10Presenting document LLL_Factorization/document
13:27:10Presenting document LLL_Factorization/outline
13:27:10Presenting theory "LLL_Factorization.Factor_Bound_2"
13:27:10Presenting theory "Perron_Frobenius.Cancel_Card_Constraint"
13:27:10Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML"
13:27:10Presenting theory "Design_Theory.Multisets_Extras"
13:27:10Presenting theory "LLL_Factorization.Missing_Dvd_Int_Poly"
13:27:10Presenting theory "LLL_Factorization.LLL_Factorization_Impl"
13:27:10Presenting theory "HOL-Analysis.Urysohn"
13:27:11Presenting theory "HOL-Combinatorics.Multiset_Permutations"
13:27:11Presenting theory "Algebraic_Numbers.Resultant"
13:27:11Presenting theory "Polynomial_Factorization.Dvd_Int_Poly"
13:27:11Presenting theory "HOL-Analysis.Isolated"
13:27:12Presenting theory "LLL_Factorization.LLL_Factorization"
13:27:12Presenting theory "HOL-Analysis.Sparse_In"
13:27:12Presenting theory "Fishers_Inequality.Set_Multiset_Extras"
13:27:12Presenting theory "Well_Quasi_Orders.Least_Enum"
13:27:12Presenting theory "HOL-Analysis.Operator_Norm"
13:27:12Presenting theory "Polynomial_Factorization.Kronecker_Factorization"
13:27:12Presenting theory "LLL_Factorization.Sub_Sums"
13:27:12Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
13:27:12Presenting theory "Polynomial_Factorization.Rational_Root_Test"
13:27:13Presenting theory "Polynomial_Factorization.Gcd_Rat_Poly"
13:27:13Presenting theory "Show.Show_Poly"
13:27:13Presenting theory "HOL-Analysis.Extended_Real_Limits"
13:27:14Presenting theory "LLL_Basis_Reduction.Missing_Lemmas"
13:27:14Presenting theory "LLL_Factorization.Factorization_Algorithm_16_22"
13:27:14Presenting theory "Open_Induction.Restricted_Predicates"
13:27:14Presenting theory "LLL_Basis_Reduction.More_IArray"
13:27:14Presenting theory "LLL_Factorization.Modern_Computer_Algebra_Problem"
13:27:14Presenting Coppersmith_Method in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coppersmith_Method" ...
13:27:14Presenting document Coppersmith_Method/document
13:27:14Presenting document Coppersmith_Method/outline
13:27:14Presenting theory "Polynomial_Factorization.Rational_Factorization"
13:27:15Presenting theory "HOL-Analysis.Summation_Tests"
13:27:15Presenting theory "Coppersmith_Method.More_LLL"
13:27:15Presenting theory "Coppersmith_Method.Coppersmith_Algorithm"
13:27:15Presenting theory "HOL-Analysis.L2_Norm"
13:27:15Presenting theory "Coppersmith_Method.Howgrave_Graham"
13:27:15Presenting theory "Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp"
13:27:15Presenting theory "LLL_Basis_Reduction.Norms"
13:27:16Presenting theory "Well_Quasi_Orders.Almost_Full"
13:27:16Presenting theory "LLL_Basis_Reduction.Int_Rat_Operations"
13:27:16Presenting theory "LLL_Basis_Reduction.Cost"
13:27:16Presenting theory "HOL-Analysis.Uniform_Limit"
13:27:16Presenting theory "Well_Quasi_Orders.Minimal_Elements"
13:27:16Presenting theory "LLL_Basis_Reduction.List_Representation"
13:27:16Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
13:27:16Presenting theory "Coppersmith_Method.Coppersmith_Generic"
13:27:16Presenting theory "Berlekamp_Zassenhaus.Suitable_Prime"
13:27:17Presenting theory "HOL-Analysis.Homeomorphism"
13:27:17Presenting theory "Polynomials.MPoly_Type_Class"
13:27:17Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
13:27:17Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
13:27:17Presenting theory "Coppersmith_Method.Towards_Coppersmith"
13:27:17Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
13:27:17Presenting theory "Efficient-Mergesort.Efficient_Sort"
13:27:17Presenting theory "HOL-Analysis.Operator_Norm"
13:27:18Presenting theory "HOL-Analysis.Bounded_Linear_Function"
13:27:18Presenting theory "Polynomials.Utils"
13:27:18Presenting theory "Polynomials.MPoly_Type_Class_FMap"
13:27:19Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide_Code"
13:27:19Presenting theory "Factor_Algebraic_Polynomial.MPoly_Container"
13:27:19Presenting theory "Berlekamp_Zassenhaus.Degree_Bound"
13:27:19Presenting theory "Factor_Algebraic_Polynomial.Multivariate_Resultant"
13:27:19Presenting theory "Factor_Algebraic_Polynomial.Is_Int_To_Int"
13:27:19Presenting theory "Coppersmith_Method.Coppersmith"
13:27:19Presenting theory "Coppersmith_Method.Coppersmith_Examples"
13:27:19Presenting Linear_Inequalities in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Inequalities" ...
13:27:19Presenting document Linear_Inequalities/document
13:27:19Presenting document Linear_Inequalities/outline
13:27:19Presenting theory "Polynomials.MPoly_Type"
13:27:20Presenting theory "Linear_Inequalities.Missing_Matrix"
13:27:21Presenting theory "Linear_Inequalities.Missing_VS_Connect"
13:27:21Presenting theory "Linear_Inequalities.Basis_Extension"
13:27:21Presenting theory "Linear_Inequalities.Sum_Vec_Set"
13:27:21Presenting theory "HOL-Analysis.Extended_Real_Limits"
13:27:21Presenting theory "Berlekamp_Zassenhaus.Mahler_Measure"
13:27:21Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
13:27:21Presenting theory "Polynomials.More_MPoly_Type"
13:27:21Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly"
13:27:22Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl"
13:27:22Presenting theory "Linear_Inequalities.Integral_Bounded_Vectors"
13:27:22Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
13:27:22Presenting theory "Factor_Algebraic_Polynomial.Roots_via_IA"
13:27:23Presenting theory "HOL-Analysis.Summation_Tests"
13:27:23Presenting theory "LLL_Basis_Reduction.Gram_Schmidt_2"
13:27:23Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly"
13:27:23Presenting theory "Berlekamp_Zassenhaus.Factor_Bound"
13:27:23Presenting theory "Factor_Algebraic_Polynomial.Factor_Complex_Poly"
13:27:24Presenting theory "Linear_Inequalities.Cone"
13:27:24Presenting theory "Factor_Algebraic_Polynomial.Factor_Real_Poly"
13:27:24Presenting LP_Duality in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LP_Duality" ...
13:27:24Presenting document LP_Duality/document
13:27:24Presenting document LP_Duality/outline
13:27:24Presenting theory "LP_Duality.Minimum_Maximum"
13:27:25Presenting theory "LLL_Basis_Reduction.Gram_Schmidt_Int"
13:27:25Presenting theory "Berlekamp_Zassenhaus.Sublist_Iteration"
13:27:25Presenting theory "LP_Duality.LP_Duality"
13:27:25Presenting theory "Linear_Inequalities.Convex_Hull"
13:27:25Presenting Linear_Recurrences_Solver in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences_Solver" ...
13:27:26Presenting theory "HOL-Analysis.Derivative"
13:27:26Presenting theory "Linear_Inequalities.Normal_Vector"
13:27:27Presenting theory "Linear_Inequalities.Dim_Span"
13:27:27Presenting theory "Linear_Recurrences.RatFPS"
13:27:27Presenting theory "HOL-Combinatorics.Stirling"
13:27:27Presenting theory "Linear_Recurrences.Pochhammer_Polynomials"
13:27:28Presenting theory "Linear_Recurrences.Linear_Recurrences_Misc"
13:27:28Presenting theory "LLL_Basis_Reduction.LLL"
13:27:28Presenting theory "Linear_Recurrences.Partial_Fraction_Decomposition"
13:27:28Presenting theory "HOL-Analysis.Infinite_Sum"
13:27:28Presenting theory "Linear_Recurrences.Factorizations"
13:27:29Presenting theory "HOL-Analysis.Cartesian_Euclidean_Space"
13:27:29Presenting theory "Linear_Recurrences.Rational_FPS_Solver"
13:27:29Presenting theory "Linear_Recurrences.Linear_Recurrences_Common"
13:27:29Presenting theory "Polynomials.Power_Products"
13:27:29Presenting theory "Linear_Recurrences.Linear_Homogenous_Recurrences"
13:27:29Presenting theory "Berlekamp_Zassenhaus.Reconstruction"
13:27:29Presenting theory "Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities"
13:27:29Presenting theory "Linear_Recurrences.Eulerian_Polynomials"
13:27:30Presenting theory "Berlekamp_Zassenhaus.Code_Abort_Gcd"
13:27:30Presenting theory "Linear_Recurrences.Linear_Inhomogenous_Recurrences"
13:27:30Presenting theory "Deriving.Compare_Rat"
13:27:30Presenting theory "Deriving.Compare_Real"
13:27:30Presenting theory "Berlekamp_Zassenhaus.Berlekamp_Zassenhaus"
13:27:30Presenting theory "Linear_Inequalities.Farkas_Lemma"
13:27:30Presenting theory "Linear_Inequalities.Farkas_Minkowsky_Weyl"
13:27:30Presenting theory "Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl"
13:27:31Presenting theory "Algebraic_Numbers.Algebraic_Numbers_Prelim"
13:27:31Presenting theory "HOL-Analysis.Uniform_Limit"
13:27:31Presenting theory "Polynomials.More_Modules"
13:27:31Presenting theory "HOL-Analysis.Complex_Analysis_Basics"
13:27:31Presenting theory "Linear_Inequalities.Decomposition_Theorem"
13:27:32Presenting theory "Algebraic_Numbers.Bivariate_Polynomials"
13:27:32Presenting theory "Linear_Inequalities.Mixed_Integer_Solutions"
13:27:32Presenting theory "Polynomials.Polynomials"
13:27:32Presenting theory "Linear_Inequalities.Integer_Hull"
13:27:33Presenting Perfect_Fields in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perfect_Fields" ...
13:27:33Presenting document Perfect_Fields/document
13:27:33Presenting document Perfect_Fields/outline
13:27:33Presenting theory "LLL_Basis_Reduction.LLL_Impl"
13:27:33Presenting theory "Algebraic_Numbers.Resultant"
13:27:33Presenting theory "HOL-Analysis.Bounded_Linear_Function"
13:27:33Presenting theory "Perfect_Fields.Perfect_Fields"
13:27:33Presenting theory "Perfect_Fields.Perfect_Field_Altdef"
13:27:33Presenting Elimination_Of_Repeated_Factors in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Elimination_Of_Repeated_Factors" ...
13:27:33Presenting document Elimination_Of_Repeated_Factors/document
13:27:33Presenting document Elimination_Of_Repeated_Factors/outline
13:27:33Presenting theory "Mason_Stothers.Mason_Stothers"
13:27:34Presenting theory "Elimination_Of_Repeated_Factors.ERF_Library"
13:27:34Presenting theory "Berlekamp_Zassenhaus.Square_Free_Factorization_Int"
13:27:34Presenting theory "Elimination_Of_Repeated_Factors.ERF_Perfect_Field_Factorization"
13:27:34Presenting theory "Elimination_Of_Repeated_Factors.ERF_Algorithm"
13:27:34Presenting theory "Algebraic_Numbers.Algebraic_Numbers"
13:27:35Presenting theory "Elimination_Of_Repeated_Factors.ERF_Code_Fixes"
13:27:35Presenting theory "Elimination_Of_Repeated_Factors.ERF_Code_Test"
13:27:35Presenting Localization_Ring in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Localization_Ring" ...
13:27:35Presenting document Localization_Ring/document
13:27:35Presenting document Localization_Ring/outline
13:27:35Presenting theory "Pure-ex.Guess"
13:27:36Presenting theory "LLL_Basis_Reduction.LLL_Complexity"
13:27:36Presenting theory "Localization_Ring.Localization"
13:27:36Presenting theory "Sturm_Sequences.Misc_Polynomial"
13:27:36Presenting theory "Sturm_Sequences.Sturm_Library"
13:27:37Presenting Mersenne_Primes in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Mersenne_Primes" ...
13:27:37Presenting document Mersenne_Primes/document
13:27:37Presenting document Mersenne_Primes/outline
13:27:37Presenting theory "Berlekamp_Zassenhaus.Factorize_Int_Poly"
13:27:37Presenting theory "HOL-Number_Theory.Fib"
13:27:37Presenting theory "Polynomials.MPoly_Type_Class"
13:27:38Presenting theory "HOL-Number_Theory.Cong"
13:27:38Presenting theory "Berlekamp_Zassenhaus.Factorize_Rat_Poly"
13:27:38Presenting theory "Sturm_Sequences.Sturm_Theorem"
13:27:38Presenting theory "HOL-Number_Theory.Totient"
13:27:38Presenting theory "Berlekamp_Zassenhaus.Factorization_External_Interface"
13:27:38Presenting Orbit_Stabiliser in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Orbit_Stabiliser" ...
13:27:38Presenting document Orbit_Stabiliser/document
13:27:38Presenting document Orbit_Stabiliser/outline
13:27:38Presenting theory "HOL-Number_Theory.Residues"
13:27:38Presenting theory "Algebraic_Numbers.Sturm_Rat"
13:27:39Presenting theory "HOL-Number_Theory.Eratosthenes"
13:27:39Presenting theory "HOL-Number_Theory.Mod_Exp"
13:27:39Presenting theory "Algebraic_Numbers.Factors_of_Int_Poly"
13:27:39Presenting theory "Algebraic_Numbers.Min_Int_Poly"
13:27:39Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:27:39Presenting theory "Orbit_Stabiliser.Orbit_Stabiliser"
13:27:39Presenting theory "Algebraic_Numbers.Algebraic_Numbers_Pre_Impl"
13:27:39Presenting theory "HOL-Number_Theory.Gauss"
13:27:40Presenting theory "Algebraic_Numbers.Cauchy_Root_Bound"
13:27:40Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:27:40Presenting theory "LLL_Basis_Reduction.LLL_Number_Bounds"
13:27:41Presenting theory "HOL-Analysis.Complex_Transcendental"
13:27:41Presenting theory "HOL-Number_Theory.Pocklington"
13:27:42Presenting theory "HOL-Number_Theory.Prime_Powers"
13:27:43Presenting theory "Orbit_Stabiliser.Tetrahedron"
13:27:43Presenting theory "LLL_Basis_Reduction.LLL_Certification"
13:27:43Presenting Padic_Ints in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Padic_Ints" ...
13:27:43Presenting document Padic_Ints/document
13:27:43Presenting document Padic_Ints/outline
13:27:43Presenting theory "LLL_Basis_Reduction.FPLLL_Solver"
13:27:43Presenting Padic_Field in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Padic_Field" ...
13:27:43Presenting document Padic_Field/document
13:27:43Presenting document Padic_Field/outline
13:27:44Presenting theory "Algebraic_Numbers.Real_Algebraic_Numbers"
13:27:44Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:27:44Presenting theory "HOL-Number_Theory.Number_Theory"
13:27:44Presenting theory "Probabilistic_Prime_Tests.Legendre_Symbol"
13:27:44Presenting theory "Probabilistic_Prime_Tests.Algebraic_Auxiliaries"
13:27:45Presenting theory "Algebraic_Numbers.Real_Roots"
13:27:45Presenting theory "Probabilistic_Prime_Tests.Jacobi_Symbol"
13:27:45Presenting theory "Algebraic_Numbers.Complex_Roots_Real_Poly"
13:27:45Presenting theory "HOL-Analysis.Derivative"
13:27:45Presenting theory "Algebraic_Numbers.Compare_Complex"
13:27:45Presenting theory "Mersenne_Primes.Lucas_Lehmer_Auxiliary"
13:27:46Presenting theory "Algebraic_Numbers.Interval_Arithmetic"
13:27:47Presenting theory "Pell.Pell"
13:27:47Presenting theory "Padic_Ints.Function_Ring"
13:27:47Presenting theory "Algebraic_Numbers.Complex_Algebraic_Numbers"
13:27:47Presenting theory "Polynomials.MPoly_Type"
13:27:48Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
13:27:48Presenting theory "Polynomials.More_MPoly_Type"
13:27:48Presenting theory "Mersenne_Primes.Lucas_Lehmer"
13:27:48Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
13:27:48Presenting theory "HOL-Analysis.Sigma_Algebra"
13:27:48Presenting theory "Polynomials.MPoly_Type_Univariate"
13:27:49Presenting theory "Native_Word.Code_Int_Integer_Conversion"
13:27:49Presenting theory "Localization_Ring.Localization"
13:27:49Presenting theory "Word_Lib.More_Arithmetic"
13:27:49Presenting theory "Symmetric_Polynomials.Vieta"
13:27:49Presenting theory "Word_Lib.More_Divides"
13:27:49Presenting theory "Word_Lib.More_Bit_Ring"
13:27:50Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
13:27:51Presenting theory "Groebner_Bases.General"
13:27:51Presenting theory "Word_Lib.More_Word"
13:27:51Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
13:27:52Presenting theory "Groebner_Bases.More_MPoly_Type_Class"
13:27:52Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
13:27:52Presenting theory "Word_Lib.Most_significant_bit"
13:27:52Presenting theory "Word_Lib.Least_significant_bit"
13:27:52Presenting theory "Word_Lib.Generic_set_bit"
13:27:52Presenting theory "Word_Lib.Bit_Comprehension"
13:27:52Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
13:27:52Presenting theory "Native_Word.Code_Target_Integer_Bit"
13:27:52Presenting theory "Native_Word.Code_Target_Int_Bit"
13:27:52Presenting theory "HOL-Analysis.Measurable"
13:27:53Presenting theory "Padic_Field.Fraction_Field"
13:27:53Presenting theory "Mersenne_Primes.Lucas_Lehmer_Code"
13:27:53Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
13:27:53Presenting file "~~/src/HOL/Analysis/measurable.ML"
13:27:53Presenting theory "Polynomials.MPoly_Type_Class_FMap"
13:27:53Presenting theory "Well_Quasi_Orders.Least_Enum"
13:27:53Presenting Perfect-Number-Thm in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perfect-Number-Thm" ...
13:27:53Presenting document Perfect-Number-Thm/document
13:27:53Presenting document Perfect-Number-Thm/outline
13:27:53Presenting theory "Perfect-Number-Thm.PerfectBasics"
13:27:53Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
13:27:53Presenting theory "Perfect-Number-Thm.Sigma"
13:27:53Presenting theory "Perfect-Number-Thm.Perfect"
13:27:53Presenting Polynomial_Factorization in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Polynomial_Factorization" ...
13:27:53Presenting document Polynomial_Factorization/document
13:27:53Presenting document Polynomial_Factorization/outline
13:27:53Presenting theory "Open_Induction.Restricted_Predicates"
13:27:53Presenting theory "Matrix.Utility"
13:27:54Presenting theory "Well_Quasi_Orders.Almost_Full"
13:27:54Presenting theory "Well_Quasi_Orders.Minimal_Elements"
13:27:54Presenting theory "Virtual_Substitution.MPolyExtension"
13:27:54Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
13:27:54Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
13:27:55Presenting theory "Polynomials.Utils"
13:27:55Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
13:27:55Presenting theory "HOL-Analysis.Brouwer_Fixpoint"
13:27:55Presenting theory "Polynomial_Factorization.Missing_List"
13:27:56Presenting theory "Polynomial_Factorization.Missing_Multiset"
13:27:56Presenting theory "Containers.Containers_Auxiliary"
13:27:56Presenting theory "Groebner_Bases.Macaulay_Matrix"
13:27:56Presenting theory "Containers.List_Fusion"
13:27:57Presenting theory "Containers.Lexicographic_Order"
13:27:57Presenting theory "Containers.Extend_Partial_Order"
13:27:57Presenting theory "Polynomials.Power_Products"
13:27:58Presenting theory "Virtual_Substitution.ExecutiblePolyProps"
13:27:58Presenting theory "Polynomials.More_Modules"
13:27:59Presenting theory "Fishers_Inequality.Matrix_Vector_Extras"
13:27:59Presenting theory "Containers.Set_Linorder"
13:27:59Presenting theory "Sturm_Tarski.PolyMisc"
13:28:00Presenting theory "Design_Theory.Design_Basics"
13:28:00Presenting theory "Polynomials.MPoly_Type_Class"
13:28:00Presenting theory "Deriving.Generator_Aux"
13:28:00Presenting file "$AFP/Deriving/bnf_access.ML"
13:28:00Presenting file "$AFP/Deriving/generator_aux.ML"
13:28:00Presenting theory "Deriving.Derive_Manager"
13:28:00Presenting file "$AFP/Deriving/derive_manager.ML"
13:28:00Presenting theory "Containers.Containers_Generator"
13:28:00Presenting file "$AFP/Containers/containers_generator.ML"
13:28:01Presenting theory "Deriving.Comparator"
13:28:01Presenting theory "Design_Theory.Design_Operations"
13:28:01Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
13:28:01Presenting theory "HOL-Analysis.Determinants"
13:28:01Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide"
13:28:02Presenting theory "Design_Theory.Block_Designs"
13:28:03Presenting theory "Deriving.Comparator_Generator"
13:28:03Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
13:28:03Presenting theory "Deriving.Compare"
13:28:03Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
13:28:04Presenting theory "Deriving.Compare_Generator"
13:28:04Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
13:28:04Presenting theory "Deriving.Compare_Instances"
13:28:05Presenting theory "Containers.Collection_Order"
13:28:05Presenting file "$AFP/Containers/ccompare_generator.ML"
13:28:05Presenting theory "Design_Theory.BIBD"
13:28:06Presenting theory "Containers.RBT_ext"
13:28:06Presenting theory "Fishers_Inequality.Design_Extras"
13:28:07Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
13:28:07Presenting theory "Sturm_Tarski.Sturm_Tarski"
13:28:07Presenting theory "HOL-Analysis.Measure_Space"
13:28:07Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
13:28:07Presenting theory "Deriving.RBT_Comparator_Impl"
13:28:07Presenting theory "List-Index.List_Index"
13:28:08Presenting theory "Containers.RBT_Mapping2"
13:28:08Presenting theory "Design_Theory.Sub_Designs"
13:28:08Presenting theory "Padic_Ints.Cring_Poly"
13:28:08Presenting theory "Polynomials.MPoly_Type_Class_FMap"
13:28:08Presenting theory "Containers.RBT_Set2"
13:28:08Presenting theory "Polynomial_Factorization.Precomputation"
13:28:08Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide_Code"
13:28:08Presenting theory "Factor_Algebraic_Polynomial.MPoly_Container"
13:28:08Presenting theory "Factor_Algebraic_Polynomial.Multivariate_Resultant"
13:28:09Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:28:09Presenting theory "Factor_Algebraic_Polynomial.Is_Int_To_Int"
13:28:09Presenting theory "Design_Theory.Design_Isomorphisms"
13:28:09Presenting theory "HOL-Eisbach.Eisbach"
13:28:09Presenting theory "Sturm_Tarski.Pseudo_Remainder_Sequence"
13:28:09Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
13:28:09Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
13:28:09Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
13:28:09Presenting file "~~/src/HOL/Eisbach/match_method.ML"
13:28:09Presenting theory "Padic_Ints.Supplementary_Ring_Facts"
13:28:10Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:28:10Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:28:10Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:28:10Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:28:10Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:28:10Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:28:10Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:28:10Presenting theory "Polynomial_Factorization.Order_Polynomial"
13:28:11Presenting theory "Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary"
13:28:11Presenting theory "Matrix.Utility"
13:28:11Presenting theory "Virtual_Substitution.PolyAtoms"
13:28:11Presenting theory "Sqrt_Babylonian.Log_Impl"
13:28:11Presenting theory "Polynomial_Factorization.Polynomial_Irreducibility"
13:28:11Presenting theory "Padic_Ints.Extended_Int"
13:28:12Presenting theory "Padic_Field.Cring_Multivariable_Poly"
13:28:12Presenting theory "Cauchy.CauchysMeanTheorem"
13:28:12Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly"
13:28:12Presenting theory "HOL-Number_Theory.Cong"
13:28:12Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl"
13:28:13Presenting theory "Sqrt_Babylonian.NthRoot_Impl"
13:28:13Presenting theory "HOL-Number_Theory.Totient"
13:28:13Presenting theory "Padic_Field.Indices"
13:28:13Presenting theory "HOL-Number_Theory.Residues"
13:28:13Presenting theory "Factor_Algebraic_Polynomial.Roots_via_IA"
13:28:13Presenting theory "Sqrt_Babylonian.Sqrt_Babylonian"
13:28:13Presenting theory "Fishers_Inequality.Incidence_Matrices"
13:28:14Presenting theory "HOL-Analysis.Borel_Space"
13:28:14Presenting theory "Polynomial_Factorization.Explicit_Roots"
13:28:14Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly"
13:28:15Presenting theory "Padic_Ints.Padic_Construction"
13:28:15Presenting theory "Factor_Algebraic_Polynomial.Factor_Complex_Poly"
13:28:15Presenting theory "Polynomial_Factorization.Square_Free_Factorization"
13:28:15Presenting theory "Virtual_Substitution.Debruijn"
13:28:15Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:28:15Presenting theory "Fishers_Inequality.Dual_Systems"
13:28:15Presenting theory "Linear_Recurrences_Solver.Linear_Recurrences_Solver"
13:28:15Presenting theory "Show.Show_Real"
13:28:15Presenting theory "Show.Show_Complex"
13:28:16Presenting theory "Linear_Recurrences_Solver.Linear_Recurrences_Pretty"
13:28:16Presenting theory "Algebraic_Numbers.Show_Real_Alg"
13:28:17Presenting theory "Virtual_Substitution.Optimizations"
13:28:17Presenting theory "Algebraic_Numbers.Show_Real_Precise"
13:28:17Presenting theory "HOL-Analysis.Cartesian_Euclidean_Space"
13:28:17Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:28:17Presenting theory "Linear_Recurrences_Solver.Show_RatFPS"
13:28:17Presenting theory "Polynomial_Interpolation.Divmod_Int"
13:28:17Presenting theory "Linear_Recurrences_Solver.Linear_Recurrences_Test"
13:28:17Presenting theory "Rank_Nullity_Theorem.Dual_Order"
13:28:17Presenting Secondary_Sylow in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Secondary_Sylow" ...
13:28:17Presenting document Secondary_Sylow/document
13:28:17Presenting document Secondary_Sylow/outline
13:28:17Presenting theory "Polynomial_Interpolation.Is_Rat_To_Rat"
13:28:17Presenting theory "Padic_Ints.Padic_Integers"
13:28:18Presenting theory "Rank_Nullity_Theorem.Mod_Type"
13:28:18Presenting theory "Polynomial_Factorization.Dvd_Int_Poly"
13:28:18Presenting theory "Polynomial_Factorization.Missing_Polynomial_Factorial"
13:28:18Presenting theory "Secondary_Sylow.GroupAction"
13:28:19Presenting theory "Rank_Nullity_Theorem.Miscellaneous"
13:28:19Presenting theory "Polynomial_Factorization.Gauss_Lemma"
13:28:19Presenting theory "Pure-ex.Guess"
13:28:19Presenting theory "BenOr_Kozen_Reif.More_Matrix"
13:28:20Presenting theory "Secondary_Sylow.SubgroupConjugation"
13:28:20Presenting theory "Polynomial_Factorization.Prime_Factorization"
13:28:20Presenting theory "Virtual_Substitution.VSAlgos"
13:28:20Presenting theory "Polynomial_Factorization.Rational_Root_Test"
13:28:20Presenting theory "Secondary_Sylow.SndSylow"
13:28:20Presenting theory "Padic_Ints.Padic_Int_Topology"
13:28:20Presenting theory "Polynomial_Interpolation.Improved_Code_Equations"
13:28:20Presenting UTP-Toolkit in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UTP-Toolkit" ...
13:28:20Presenting document UTP-Toolkit/document
13:28:20Presenting document UTP-Toolkit/outline
13:28:21Presenting theory "Padic_Ints.Padic_Int_Polynomials"
13:28:21Presenting theory "Fishers_Inequality.Rank_Argument_General"
13:28:21Presenting theory "Fishers_Inequality.Linear_Bound_Argument"
13:28:21Presenting theory "Polynomial_Interpolation.Newton_Interpolation"
13:28:21Presenting theory "Sturm_Sequences.Misc_Polynomial"
13:28:21Presenting theory "Sturm_Sequences.Sturm_Library"
13:28:21Presenting theory "Virtual_Substitution.LinearCase"
13:28:22Presenting theory "Polynomial_Interpolation.Lagrange_Interpolation"
13:28:22Presenting theory "Fishers_Inequality.Fishers_Inequality"
13:28:22Presenting theory "HOL-Analysis.Nonnegative_Lebesgue_Integration"
13:28:23Presenting theory "Polynomial_Interpolation.Neville_Aitken_Interpolation"
13:28:23Presenting theory "Polynomial_Interpolation.Polynomial_Interpolation"
13:28:24Presenting theory "HOL-Eisbach.Eisbach"
13:28:24Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
13:28:24Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
13:28:24Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
13:28:24Presenting file "~~/src/HOL/Eisbach/match_method.ML"
13:28:24Presenting theory "Fishers_Inequality.Vector_Matrix_Mod"
13:28:24Presenting theory "Padic_Field.Ring_Powers"
13:28:24Presenting theory "Optics.Two"
13:28:24Presenting theory "Optics.Interp"
13:28:25Presenting theory "Optics.Lens_Laws"
13:28:25Presenting theory "Optics.Lens_Algebra"
13:28:25Presenting theory "Polynomial_Factorization.Kronecker_Factorization"
13:28:25Presenting theory "Polynomial_Factorization.Polynomial_Irreducibility"
13:28:25Presenting theory "Fishers_Inequality.Fishers_Inequality_Variations"
13:28:25Presenting theory "Fishers_Inequality.Fishers_Inequality_Root"
13:28:25Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
13:28:25Presenting UTP in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UTP" ...
13:28:25Presenting document UTP/document
13:28:25Presenting document UTP/outline
13:28:25Presenting theory "Optics.Lens_Order"
13:28:25Presenting theory "Optics.Lens_Symmetric"
13:28:26Presenting theory "UTP.utp_parser_utils"
13:28:26Presenting theory "Virtual_Substitution.QuadraticCase"
13:28:26Presenting theory "Optics.Scenes"
13:28:26Presenting theory "Sturm_Sequences.Sturm_Theorem"
13:28:26Presenting theory "UTP.utp_var"
13:28:26Presenting theory "HOL-Analysis.Binary_Product_Measure"
13:28:27Presenting theory "Padic_Ints.Hensels_Lemma"
13:28:27Presenting theory "UTP.utp_expr"
13:28:27Presenting theory "Sturm_Sequences.Sturm_Method"
13:28:27Presenting file "$AFP/Sturm_Sequences/sturm.ML"
13:28:27Presenting theory "Optics.Scene_Spaces"
13:28:28Presenting theory "Perron_Frobenius.Cancel_Card_Constraint"
13:28:28Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML"
13:28:28Presenting theory "UTP.utp_expr_insts"
13:28:28Presenting theory "Perron_Frobenius.Bij_Nat"
13:28:28Presenting theory "Virtual_Substitution.EliminateVariable"
13:28:28Presenting theory "UTP.utp_expr_funcs"
13:28:28Presenting theory "Padic_Ints.Zp_Compact"
13:28:29Presenting VectorSpace in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/VectorSpace" ...
13:28:29Presenting document VectorSpace/document
13:28:29Presenting document VectorSpace/outline
13:28:29Presenting theory "Virtual_Substitution.LuckyFind"
13:28:29Presenting theory "VectorSpace.RingModuleFacts"
13:28:29Presenting theory "UTP.utp_unrest"
13:28:29Presenting theory "VectorSpace.FunctionLemmas"
13:28:29Presenting theory "Perron_Frobenius.HMA_Connect"
13:28:29Presenting theory "VectorSpace.MonoidSums"
13:28:29Presenting theory "UTP.utp_usedby"
13:28:30Presenting theory "Perron_Frobenius.Perron_Frobenius_Aux"
13:28:30Presenting theory "Virtual_Substitution.EqualityVS"
13:28:30Presenting theory "Polynomial_Factorization.Square_Free_Factorization"
13:28:30Presenting theory "Perron_Frobenius.Perron_Frobenius"
13:28:30Presenting theory "Polynomial_Factorization.Gcd_Rat_Poly"
13:28:30Presenting theory "Optics.Lens_Instances"
13:28:30Presenting file "$AFP/Optics/Lens_Lib.ML"
13:28:30Presenting file "$AFP/Optics/Lens_Record.ML"
13:28:30Presenting file "$AFP/Optics/Lens_Statespace.ML"
13:28:30Presenting theory "Optics.Lenses"
13:28:31Presenting theory "VectorSpace.LinearCombinations"
13:28:31Presenting theory "Perron_Frobenius.Roots_Unity"
13:28:31Presenting theory "UTP.utp_subst"
13:28:31Presenting theory "VectorSpace.SumSpaces"
13:28:32Presenting theory "UTP.utp_tactics"
13:28:32Presenting theory "UTP-Toolkit.List_Extra"
13:28:32Presenting file "$AFP/UTP/utp/uexpr_rep_eq.ML"
13:28:32Presenting file "$AFP/UTP/utp/utp_tactics.ML"
13:28:32Presenting theory "HOL-Analysis.Finite_Product_Measure"
13:28:32Presenting theory "Show.Show"
13:28:32Presenting theory "UTP.utp_meta_subst"
13:28:32Presenting file "$AFP/Show/show_generator.ML"
13:28:32Presenting theory "UTP-Toolkit.Sequence"
13:28:33Presenting theory "UTP-Toolkit.FSet_Extra"
13:28:33Presenting theory "Show.Show_Instances"
13:28:33Presenting theory "Show.Show_Poly"
13:28:33Presenting theory "Perron_Frobenius.Perron_Frobenius_Irreducible"
13:28:33Presenting theory "UTP-Toolkit.Countable_Set_Extra"
13:28:34Presenting theory "VectorSpace.VectorSpace"
13:28:34Presenting theory "Padic_Field.Padic_Fields"
13:28:34Presenting HOL-Number_Theory in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Number_Theory" ...
13:28:34Presenting document HOL-Number_Theory/document
13:28:34Presenting document HOL-Number_Theory/outline
13:28:34Presenting theory "UTP.utp_pred"
13:28:34Presenting theory "Polynomial_Factorization.Rational_Factorization"
13:28:34Presenting Amicable_Numbers in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Amicable_Numbers" ...
13:28:34Presenting document Amicable_Numbers/document
13:28:34Presenting document Amicable_Numbers/outline
13:28:34Presenting theory "HOL-Number_Theory.Fib"
13:28:34Presenting theory "Perron_Frobenius.Perron_Frobenius_General"
13:28:34Presenting theory "Lehmer.Lehmer"
13:28:34Presenting theory "Perron_Frobenius.Spectral_Radius_Theory"
13:28:35Presenting theory "HOL-Number_Theory.Cong"
13:28:35Presenting theory "HOL-Real_Asymp.Lazy_Eval"
13:28:35Presenting file "~~/src/HOL/Real_Asymp/lazy_eval.ML"
13:28:35Presenting theory "UTP.utp_alphabet"
13:28:35Presenting theory "HOL-Real_Asymp.Inst_Existentials"
13:28:35Presenting file "~~/src/HOL/Real_Asymp/inst_existentials.ML"
13:28:35Presenting theory "HOL-Real_Asymp.Eventuallize"
13:28:35Presenting theory "UTP.utp_lift"
13:28:35Presenting theory "HOL-Analysis.Caratheodory"
13:28:35Presenting theory "HOL-Algebra.Congruence"
13:28:36Presenting theory "HOL-Algebra.Order"
13:28:36Presenting theory "UTP-Toolkit.Map_Extra"
13:28:36Presenting theory "UTP-Toolkit.List_Lexord_Alt"
13:28:36Presenting theory "HOL-Algebra.Lattice"
13:28:37Presenting theory "UTP-Toolkit.Partial_Fun"
13:28:38Presenting theory "UTP.utp_pred_laws"
13:28:38Presenting theory "HOL-Algebra.Complete_Lattice"
13:28:38Presenting theory "UTP-Toolkit.Finite_Fun"
13:28:38Presenting theory "Pratt_Certificate.Pratt_Certificate"
13:28:39Presenting theory "UTP-Toolkit.Infinity"
13:28:39Presenting file "$AFP/Pratt_Certificate/pratt.ML"
13:28:39Presenting theory "Pratt_Certificate.Pratt_Certificate_Code"
13:28:39Presenting theory "UTP-Toolkit.Positive"
13:28:39Presenting theory "UTP.utp_healthy"
13:28:39Presenting theory "Matrix.Utility"
13:28:39Presenting theory "HOL-Algebra.Group"
13:28:40Presenting theory "UTP-Toolkit.Total_Recall"
13:28:40Presenting file "$AFP/UTP/toolkit/Total_Recall.ML"
13:28:40Presenting theory "UTP-Toolkit.utp_toolkit"
13:28:40Presenting Arith_Prog_Rel_Primes in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Arith_Prog_Rel_Primes" ...
13:28:40Presenting document Arith_Prog_Rel_Primes/document
13:28:40Presenting document Arith_Prog_Rel_Primes/outline
13:28:42Presenting theory "UTP.utp_rel"
13:28:43Presenting theory "UTP.utp_recursion"
13:28:43Presenting theory "UTP.utp_sequent"
13:28:43Presenting theory "HOL-Algebra.Coset"
13:28:43Presenting theory "Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes"
13:28:43Presenting Bertrands_Postulate in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bertrands_Postulate" ...
13:28:43Presenting document Bertrands_Postulate/document
13:28:43Presenting document Bertrands_Postulate/outline
13:28:44Presenting theory "Polynomial_Factorization.Missing_List"
13:28:44Presenting theory "HOL-Algebra.FiniteProduct"
13:28:44Presenting theory "Polynomial_Factorization.Missing_Multiset"
13:28:45Presenting theory "HOL-Real_Asymp.Multiseries_Expansion"
13:28:45Presenting theory "UTP.utp_rel_laws"
13:28:45Presenting file "~~/src/HOL/Real_Asymp/asymptotic_basis.ML"
13:28:45Presenting file "~~/src/HOL/Real_Asymp/exp_log_expression.ML"
13:28:46Presenting file "~~/src/HOL/Real_Asymp/expansion_interface.ML"
13:28:46Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion.ML"
13:28:46Presenting theory "HOL-Algebra.Ring"
13:28:46Presenting file "~~/src/HOL/Real_Asymp/real_asymp.ML"
13:28:46Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:28:46Presenting theory "Polynomial_Factorization.Prime_Factorization"
13:28:46Presenting theory "HOL-Decision_Procs.Dense_Linear_Order"
13:28:46Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML"
13:28:46Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML"
13:28:46Presenting file "~~/src/HOL/Decision_Procs/langford.ML"
13:28:46Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"
13:28:47Presenting theory "HOL-Algebra.Module"
13:28:47Presenting theory "UTP.utp_theory"
13:28:48Presenting theory "HOL-Analysis.Bochner_Integration"
13:28:48Presenting theory "UTP.utp_hoare"
13:28:48Presenting theory "UTP.utp_wp"
13:28:49Presenting theory "UTP.utp_dynlog"
13:28:49Presenting theory "UTP.utp_state_parser"
13:28:49Presenting theory "Padic_Field.Padic_Field_Polynomials"
13:28:49Presenting theory "HOL-Algebra.AbelCoset"
13:28:49Presenting theory "Amicable_Numbers.Amicable_Numbers"
13:28:49Presenting theory "UTP.utp_rel_opsem"
13:28:49Presenting theory "UTP.utp_sym_eval"
13:28:49Presenting theory "HOL-Real_Asymp.Multiseries_Expansion_Bounds"
13:28:49Presenting Crypto_Standards in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Crypto_Standards" ...
13:28:49Presenting theory "UTP.utp_sp"
13:28:49Presenting document Crypto_Standards/document
13:28:49Presenting document Crypto_Standards/outline
13:28:49Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion_bounds.ML"
13:28:49Presenting theory "Crypto_Standards.More_Bit_Operations_Nat"
13:28:50Presenting theory "HOL-Algebra.Ideal"
13:28:51Presenting theory "HOL-Algebra.RingHom"
13:28:51Presenting theory "Crypto_Standards.Words"
13:28:51Presenting theory "HOL-Real_Asymp.Real_Asymp"
13:28:51Presenting file "~~/src/HOL/Real_Asymp/real_asymp_diag.ML"
13:28:52Presenting theory "UTP.utp_concurrency"
13:28:52Presenting theory "UTP.utp"
13:28:52Presenting theory "Padic_Field.Padic_Field_Topology"
13:28:52Presenting theory "UTP.utp_expr_ovld"
13:28:52Presenting theory "UTP.utp_full"
13:28:53Presenting theory "UTP.utp_easy_parser"
13:28:53Presenting theory "UTP.sum_list"
13:28:53Presenting theory "UTP.utp_simple_time"
13:28:53Presenting DigitsInBase in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DigitsInBase" ...
13:28:53Presenting document DigitsInBase/document
13:28:53Presenting document DigitsInBase/outline
13:28:53Presenting theory "Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block"
13:28:53Presenting theory "HOL-Analysis.Complete_Measure"
13:28:53Presenting theory "HOL-Decision_Procs.Approximation_Bounds"
13:28:54Presenting theory "Perron_Frobenius.Hom_Gauss_Jordan"
13:28:54Presenting theory "Perron_Frobenius.Spectral_Radius_Theory_2"
13:28:54Presenting theory "Perron_Frobenius.Check_Matrix_Growth"
13:28:54Presenting Elliptic_Curves_Group_Law in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Elliptic_Curves_Group_Law" ...
13:28:54Presenting document Elliptic_Curves_Group_Law/document
13:28:54Presenting document Elliptic_Curves_Group_Law/outline
13:28:54Presenting theory "Crypto_Standards.PKCS1v2_2"
13:28:54Presenting theory "Lehmer.Lehmer"
13:28:54Presenting theory "HOL-Algebra.UnivPoly"
13:28:55Presenting theory "DigitsInBase.DigitsInBase"
13:28:55Presenting theory "HOL-Algebra.Generated_Groups"
13:28:55Presenting theory "Padic_Field.Generated_Boolean_Algebra"
13:28:55Presenting Fermat3_4 in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fermat3_4" ...
13:28:55Presenting document Fermat3_4/document
13:28:55Presenting document Fermat3_4/outline
13:28:56Presenting theory "HOL-Analysis.Regularity"
13:28:56Presenting theory "Crypto_Standards.FIPS180_4"
13:28:56Presenting theory "HOL-Algebra.Elementary_Groups"
13:28:57Presenting theory "HOL-Decision_Procs.Conversions"
13:28:57Presenting theory "Crypto_Standards.PKCS1v2_2_Interpretations"
13:28:57Presenting theory "Crypto_Standards.FIPS198_1"
13:28:57Presenting theory "HOL-Algebra.Multiplicative_Group"
13:28:58Presenting theory "Fermat3_4.Fermat4"
13:28:58Presenting theory "HOL-Number_Theory.Totient"
13:28:58Presenting theory "Pratt_Certificate.Pratt_Certificate"
13:28:58Presenting file "$AFP/Pratt_Certificate/pratt.ML"
13:28:58Presenting theory "HOL-Number_Theory.Residues"
13:28:58Presenting theory "HOL-Decision_Procs.Algebra_Aux"
13:28:58Presenting theory "HOL-Decision_Procs.Conversions"
13:28:58Presenting theory "HOL-Decision_Procs.Algebra_Aux"
13:28:58Presenting theory "HOL-Number_Theory.Eratosthenes"
13:28:59Presenting theory "HOL-Number_Theory.Mod_Exp"
13:28:59Presenting theory "HOL-Number_Theory.Euler_Criterion"
13:28:59Presenting theory "HOL-Number_Theory.Gauss"
13:28:59Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
13:29:00Presenting theory "HOL-Decision_Procs.Commutative_Ring"
13:29:00Presenting theory "HOL-Number_Theory.Pocklington"
13:29:01Presenting theory "HOL-Analysis.Lebesgue_Measure"
13:29:01Presenting theory "HOL-Decision_Procs.Reflective_Field"
13:29:01Presenting theory "HOL-Number_Theory.Prime_Powers"
13:29:02Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
13:29:02Presenting theory "HOL-Decision_Procs.Commutative_Ring"
13:29:02Presenting theory "HOL-Number_Theory.Number_Theory"
13:29:02Presenting Gaussian_Integers in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gaussian_Integers" ...
13:29:02Presenting document Gaussian_Integers/document
13:29:02Presenting document Gaussian_Integers/outline
13:29:03Presenting theory "Gaussian_Integers.Gaussian_Integers"
13:29:04Presenting theory "Matrix.Utility"
13:29:04Presenting theory "Elliptic_Curves_Group_Law.Elliptic_Locale"
13:29:04Presenting theory "Fermat3_4.Quad_Form"
13:29:04Presenting theory "Elliptic_Curves_Group_Law.Elliptic_Test"
13:29:05Presenting theory "Crypto_Standards.More_Residues"
13:29:05Presenting theory "Bertrands_Postulate.Bertrand"
13:29:05Presenting theory "Polynomial_Factorization.Missing_List"
13:29:05Presenting file "$AFP/Bertrands_Postulate/bertrand.ML"
13:29:05Presenting HOL-ex in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-ex" ...
13:29:05Presenting theory "HOL-Decision_Procs.Reflective_Field"
13:29:05Presenting theory "Polynomial_Factorization.Missing_Multiset"
13:29:05Presenting theory "HOL-ex.Antiquote"
13:29:06Presenting theory "Crypto_Standards.EC_Common"
13:29:06Presenting theory "Polynomial_Factorization.Prime_Factorization"
13:29:06Presenting theory "Gaussian_Integers.Gaussian_Integers_Test"
13:29:06Presenting theory "Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares"
13:29:06Presenting theory "Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples"
13:29:06Presenting theory "Gaussian_Integers.Gaussian_Integers_Everything"
13:29:06Presenting Kneser_Cauchy_Davenport in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kneser_Cauchy_Davenport" ...
13:29:06Presenting document Kneser_Cauchy_Davenport/document
13:29:06Presenting document Kneser_Cauchy_Davenport/outline
13:29:07Presenting theory "Jacobson_Basic_Algebra.Set_Theory"
13:29:07Presenting theory "Fermat3_4.Fermat3"
13:29:07Presenting Koenigsberg_Friendship in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Koenigsberg_Friendship" ...
13:29:07Presenting document Koenigsberg_Friendship/document
13:29:07Presenting document Koenigsberg_Friendship/outline
13:29:08Presenting theory "Jacobson_Basic_Algebra.Group_Theory"
13:29:09Presenting theory "Dijkstra_Shortest_Path.Graph"
13:29:09Presenting theory "Crypto_Standards.SEC1v2_0"
13:29:09Presenting theory "Crypto_Standards.Crypto_Standards"
13:29:09Presenting theory "Crypto_Standards.Efficient_Mod_Exp"
13:29:09Presenting theory "HOL-Analysis.Tagged_Division"
13:29:09Presenting theory "Jacobson_Basic_Algebra.Ring_Theory"
13:29:10Presenting theory "HOL-ex.Argo_Examples"
13:29:10Presenting theory "Elliptic_Curves_Group_Law.Elliptic_Axclass"
13:29:11Presenting theory "HOL-ex.Arith_Examples"
13:29:11Presenting theory "Crypto_Standards.PKCS1v2_2_Test_Vectors"
13:29:11Presenting theory "Crypto_Standards.FIPS180_4_Test_Vectors"
13:29:12Presenting theory "HOL-ex.Ballot"
13:29:12Presenting theory "Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality"
13:29:13Presenting theory "HOL-ex.BigO"
13:29:14Presenting theory "HOL-ex.BinEx"
13:29:14Presenting theory "HOL-ex.Birthday_Paradox"
13:29:14Presenting theory "HOL-ex.Bubblesort"
13:29:15Presenting theory "HOL-ex.CTL"
13:29:16Presenting theory "Crypto_Standards.FIPS198_1_Test_Vectors"
13:29:17Presenting theory "Kneser_Cauchy_Davenport.Kneser_Cauchy_Davenport_preliminaries"
13:29:17Presenting theory "Crypto_Standards.Efficient_SEC1"
13:29:18Presenting theory "Crypto_Standards.FIPS186_4_Curves"
13:29:18Presenting theory "Elliptic_Curves_Group_Law.Elliptic_Locale"
13:29:19Presenting theory "Elliptic_Curves_Group_Law.Elliptic_Test"
13:29:19Presenting Lehmer in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lehmer" ...
13:29:19Presenting document Lehmer/document
13:29:19Presenting document Lehmer/outline
13:29:20Presenting theory "HOL-ex.Cartouche_Examples"
13:29:20Presenting theory "HOL-ex.Case_Product"
13:29:20Presenting theory "HOL-ex.Chinese"
13:29:20Presenting theory "Lehmer.Lehmer"
13:29:20Presenting Lifting_the_Exponent in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lifting_the_Exponent" ...
13:29:20Presenting document Lifting_the_Exponent/document
13:29:20Presenting document Lifting_the_Exponent/outline
13:29:20Presenting theory "Kneser_Cauchy_Davenport.Kneser_Cauchy_Davenport_main_proofs"
13:29:20Presenting Number_Theoretic_Transform in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Number_Theoretic_Transform" ...
13:29:20Presenting document Number_Theoretic_Transform/document
13:29:20Presenting document Number_Theoretic_Transform/outline
13:29:21Presenting theory "Subresultants.Binary_Exponentiation"
13:29:21Presenting theory "Lifting_the_Exponent.LTE"
13:29:21Presenting Pratt_Certificate in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pratt_Certificate" ...
13:29:21Presenting document Pratt_Certificate/document
13:29:21Presenting document Pratt_Certificate/outline
13:29:21Presenting theory "Lehmer.Lehmer"
13:29:22Presenting theory "Virtual_Substitution.QE"
13:29:22Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:29:23Presenting theory "HOL-ex.Classical"
13:29:23Presenting theory "HOL-ex.Code_Binary_Nat_examples"
13:29:23Presenting theory "HOL-ex.Code_Lazy_Demo"
13:29:23Presenting theory "HOL-ex.Code_Timing"
13:29:23Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
13:29:24Presenting theory "HOL-ex.Coercion_Examples"
13:29:24Presenting theory "Pratt_Certificate.Pratt_Certificate"
13:29:24Presenting file "$AFP/Pratt_Certificate/pratt.ML"
13:29:24Presenting theory "HOL-ex.Computations"
13:29:24Presenting theory "HOL-ex.Conditional_Parametricity_Examples"
13:29:24Presenting theory "Pratt_Certificate.Pratt_Certificate_Code"
13:29:24Presenting RSAPSS in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/RSAPSS" ...
13:29:24Presenting document RSAPSS/document
13:29:24Presenting document RSAPSS/outline
13:29:24Presenting theory "HOL-ex.Cubic_Quartic"
13:29:24Presenting theory "HOL-ex.Datatype_Record_Examples"
13:29:24Presenting theory "Koenigsberg_Friendship.MoreGraph"
13:29:24Presenting theory "HOL-ex.Erdoes_Szekeres"
13:29:24Presenting theory "HOL-ex.Eval_Examples"
13:29:24Presenting theory "HOL-ex.Executable_Relation"
13:29:25Presenting theory "HOL-ex.Execute_Choice"
13:29:25Presenting theory "HOL-ex.Function_Growth"
13:29:25Presenting theory "HOL-Analysis.Poly_Roots"
13:29:26Presenting theory "HOL-ex.Gauge_Integration"
13:29:26Presenting theory "Crypto_Standards.SEC1v2_0_Test_Vectors"
13:29:26Presenting theory "HOL-ex.HarmonicSeries"
13:29:26Presenting theory "Virtual_Substitution.NegInfinity"
13:29:26Presenting theory "HOL-ex.Hebrew"
13:29:26Presenting theory "HOL-ex.Hex_Bin_Examples"
13:29:26Presenting theory "HOL-ex.IArray_Examples"
13:29:26Presenting theory "Virtual_Substitution.Infinitesimals"
13:29:26Presenting theory "HOL-ex.Intuitionistic"
13:29:26Presenting theory "HOL-ex.Join_Theory"
13:29:27Presenting theory "HOL-ex.Lagrange"
13:29:27Presenting theory "HOL-ex.List_to_Set_Comprehension_Examples"
13:29:27Presenting theory "Virtual_Substitution.UniAtoms"
13:29:27Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
13:29:28Presenting theory "Crypto_Standards.Test_Vectors"
13:29:28Presenting SumSquares in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SumSquares" ...
13:29:28Presenting document SumSquares/document
13:29:28Presenting document SumSquares/outline
13:29:28Presenting theory "HOL-ex.LocaleTest2"
13:29:28Presenting theory "RSAPSS.Word"
13:29:28Presenting theory "HOL-ex.MergeSort"
13:29:28Presenting theory "HOL-ex.MonoidGroup"
13:29:28Presenting theory "SumSquares.TwoSquares"
13:29:28Presenting theory "HOL-ex.Multiquote"
13:29:28Presenting theory "HOL-ex.NatSum"
13:29:28Presenting theory "Virtual_Substitution.NegInfinityUni"
13:29:29Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
13:29:29Presenting theory "HOL-ex.Normalization_by_Evaluation"
13:29:29Presenting theory "SumSquares.FourSquares"
13:29:29Presenting theory "RSAPSS.WordOperations"
13:29:29Presenting theory "HOL-ex.PER"
13:29:29Presenting Zeckendorf in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeckendorf" ...
13:29:29Presenting document Zeckendorf/document
13:29:29Presenting document Zeckendorf/outline
13:29:29Presenting theory "RSAPSS.SHA1Padding"
13:29:30Presenting theory "RSAPSS.SHA1"
13:29:30Presenting theory "HOL-ex.Parallel_Example"
13:29:30Presenting theory "Berlekamp_Zassenhaus.Finite_Field"
13:29:30Presenting theory "Zeckendorf.Zeckendorf"
13:29:30Presenting theory "HOL-ex.Peano_Axioms"
13:29:30Presenting Farkas in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Farkas" ...
13:29:30Presenting document Farkas/document
13:29:30Presenting document Farkas/outline
13:29:30Presenting theory "RSAPSS.Wordarith"
13:29:30Presenting theory "Virtual_Substitution.InfinitesimalsUni"
13:29:30Presenting theory "HOL-Combinatorics.Transposition"
13:29:31Presenting theory "Number_Theoretic_Transform.Preliminary_Lemmas"
13:29:31Presenting theory "Virtual_Substitution.DNFUni"
13:29:31Presenting theory "HOL-Analysis.Henstock_Kurzweil_Integration"
13:29:32Presenting theory "Number_Theoretic_Transform.NTT"
13:29:32Presenting theory "Koenigsberg_Friendship.KoenigsbergBridge"
13:29:32Presenting theory "RSAPSS.EMSAPSS"
13:29:32Presenting theory "HOL-Combinatorics.Perm"
13:29:32Presenting theory "RSAPSS.Mod"
13:29:32Presenting theory "RSAPSS.Crypt"
13:29:32Presenting theory "RSAPSS.Pdifference"
13:29:32Presenting theory "RSAPSS.Productdivides"
13:29:33Presenting theory "RSAPSS.Cryptinverts"
13:29:33Presenting theory "HOL-ex.Perm_Fragments"
13:29:33Presenting theory "HOL-ex.PresburgerEx"
13:29:33Presenting theory "HOL-ex.Pythagoras"
13:29:33Presenting theory "HOL-ex.Quicksort"
13:29:34Presenting theory "HOL-Real_Asymp.Lazy_Eval"
13:29:34Presenting file "~~/src/HOL/Real_Asymp/lazy_eval.ML"
13:29:34Presenting theory "HOL-ex.Radix_Sort"
13:29:34Presenting theory "HOL-Real_Asymp.Inst_Existentials"
13:29:34Presenting file "~~/src/HOL/Real_Asymp/inst_existentials.ML"
13:29:34Presenting theory "HOL-Real_Asymp.Eventuallize"
13:29:34Presenting theory "Virtual_Substitution.GeneralVSProofs"
13:29:35Presenting theory "Number_Theoretic_Transform.Butterfly"
13:29:35Presenting Nominal_Myhill_Nerode in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Nominal_Myhill_Nerode" ...
13:29:35Presenting document Nominal_Myhill_Nerode/document
13:29:35Presenting document Nominal_Myhill_Nerode/outline
13:29:35Presenting theory "HOL-ex.Reflection_Examples"
13:29:35Presenting theory "Virtual_Substitution.Reindex"
13:29:35Presenting theory "RSAPSS.RSAPSS"
13:29:36Presenting theory "Farkas.Farkas"
13:29:36Presenting theory "HOL-ex.Refute_Examples"
13:29:36Presenting theory "Virtual_Substitution.OptimizationProofs"
13:29:36Presenting theory "HOL-ex.Residue_Ring"
13:29:36Presenting theory "HOL-ex.SOS"
13:29:36Presenting theory "HOL-ex.SOS_Cert"
13:29:37Presenting theory "HOL-ex.Serbian"
13:29:37Presenting theory "HOL-ex.Set_Comprehension_Pointfree_Examples"
13:29:37Presenting theory "HOL-ex.Set_Theory"
13:29:37Presenting theory "HOL-Library.FuncSet"
13:29:38Presenting theory "HOL-ex.Simproc_Tests"
13:29:38Presenting theory "Koenigsberg_Friendship.FriendshipTheory"
13:29:38Presenting theory "HOL-ex.Simps_Case_Conv_Examples"
13:29:38Presenting theory "HOL-Computational_Algebra.Factorial_Ring"
13:29:38Presenting theory "HOL-Algebra.Congruence"
13:29:38Presenting theory "HOL-ex.Sketch_and_Explore"
13:29:38Presenting theory "Polynomial_Interpolation.Ring_Hom"
13:29:39Presenting theory "Virtual_Substitution.DNF"
13:29:39Presenting theory "HOL-Combinatorics.Transposition"
13:29:39Presenting theory "HOL-ex.Sorting_Algorithms_Examples"
13:29:39Presenting theory "HOL-ex.Specifications_with_bundle_mixins"
13:29:39Presenting theory "HOL-ex.Sqrt_Script"
13:29:39Presenting theory "HOL-Algebra.Order"
13:29:39Presenting theory "Virtual_Substitution.VSQuad"
13:29:39Presenting theory "HOL-ex.Sudoku"
13:29:40Presenting theory "Padic_Field.Padic_Field_Powers"
13:29:40Presenting theory "HOL-ex.Tarski"
13:29:40Presenting theory "HOL-ex.Termination"
13:29:40Presenting theory "HOL-ex.ThreeDivides"
13:29:41Presenting theory "HOL-ex.Transfer_Debug"
13:29:41Presenting theory "HOL-Algebra.Lattice"
13:29:41Presenting theory "HOL-ex.Transfer_Int_Nat"
13:29:41Presenting theory "HOL-ex.Transitive_Closure_Table_Ex"
13:29:41Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Poly_Props"
13:29:41Presenting theory "HOL-Combinatorics.Permutations"
13:29:41Presenting theory "HOL-ex.Tree23"
13:29:41Presenting theory "HOL-ex.Triangular_Numbers"
13:29:42Presenting theory "HOL-ex.Unification"
13:29:42Presenting theory "Jordan_Normal_Form.Missing_Misc"
13:29:42Presenting theory "HOL-ex.While_Combinator_Example"
13:29:42Presenting theory "Datatype_Order_Generator.Derive_Aux"
13:29:42Presenting file "$AFP/Datatype_Order_Generator/derive_aux.ML"
13:29:42Presenting theory "HOL-Algebra.Complete_Lattice"
13:29:43Presenting theory "HOL-Algebra.Congruence"
13:29:44Presenting theory "HOL-ex.veriT_Preprocessing"
13:29:44Presenting theory "HOL-ex.SAT_Examples"
13:29:44Presenting theory "HOL-Algebra.Order"
13:29:44Presenting theory "Datatype_Order_Generator.Order_Generator"
13:29:44Presenting file "$AFP/Datatype_Order_Generator/order_generator.ML"
13:29:46Presenting theory "HOL-Algebra.Group"
13:29:46Presenting theory "HOL-Algebra.Bij"
13:29:46Presenting theory "HOL-Algebra.Lattice"
13:29:47Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Consistent_Sign_Assignments"
13:29:49Presenting theory "HOL-ex.Meson_Test"
13:29:49Presenting theory "HOL-Algebra.Complete_Lattice"
13:29:50Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Pseudo_Remainder_Sequence"
13:29:50Presenting theory "HOL-Algebra.Coset"
13:29:52Presenting theory "HOL-Algebra.Group_Action"
13:29:52Presenting theory "HOL-Algebra.Group"
13:29:53Presenting theory "HOL-Library.Adhoc_Overloading"
13:29:53Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
13:29:53Presenting theory "HOL-Algebra.FiniteProduct"
13:29:53Presenting theory "BenOr_Kozen_Reif.More_Matrix"
13:29:53Presenting theory "HOL-Real_Asymp.Multiseries_Expansion"
13:29:54Presenting theory "BenOr_Kozen_Reif.BKR_Algorithm"
13:29:54Presenting theory "HOL-Algebra.Generated_Groups"
13:29:54Presenting theory "BenOr_Kozen_Reif.Renegar_Algorithm"
13:29:54Presenting theory "HOL-Algebra.Ring"
13:29:54Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
13:29:54Presenting file "~~/src/HOL/Real_Asymp/asymptotic_basis.ML"
13:29:54Presenting file "~~/src/HOL/Real_Asymp/exp_log_expression.ML"
13:29:54Presenting theory "HOL-Library.Infinite_Set"
13:29:54Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix"
13:29:54Presenting file "~~/src/HOL/Real_Asymp/expansion_interface.ML"
13:29:54Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion.ML"
13:29:54Presenting theory "Jordan_Normal_Form.Missing_Ring"
13:29:54Presenting file "~~/src/HOL/Real_Asymp/real_asymp.ML"
13:29:54Presenting theory "Jordan_Normal_Form.Conjugate"
13:29:54Presenting theory "Virtual_Substitution.Heuristic"
13:29:55Presenting theory "HOL-Algebra.Module"
13:29:55Presenting theory "HOL-Algebra.Elementary_Groups"
13:29:56Presenting theory "Virtual_Substitution.HeuristicProofs"
13:29:56Presenting theory "Polynomials.Show_Polynomials"
13:29:57Presenting theory "Virtual_Substitution.PrettyPrinting"
13:29:57Presenting theory "Jordan_Normal_Form.Matrix"
13:29:57Presenting theory "Virtual_Substitution.Exports"
13:29:57Presenting theory "Virtual_Substitution.ExportProofs"
13:29:57Presenting theory "Farkas.Matrix_Farkas"
13:29:58Presenting theory "Farkas.Simplex_for_Reals"
13:29:58Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm"
13:29:59Presenting theory "BenOr_Kozen_Reif.Matrix_Equation_Construction"
13:29:59Presenting theory "Nominal_Myhill_Nerode.Nominal_Myhill_Nerode"
13:29:59Presenting theory "HOL-Real_Asymp.Multiseries_Expansion_Bounds"
13:29:59Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion_bounds.ML"
13:30:00Presenting theory "HOL-Real_Asymp.Real_Asymp"
13:30:00Presenting file "~~/src/HOL/Real_Asymp/real_asymp_diag.ML"
13:30:00Presenting theory "Quantifier_Elimination_Hybrid.Multiv_Tarski_Query"
13:30:01Presenting theory "HOL-Analysis.Kronecker_Approximation_Theorem"
13:30:02Presenting theory "BenOr_Kozen_Reif.BKR_Proofs"
13:30:02Presenting theory "HOL-Analysis.Weierstrass_Theorems"
13:30:03Presenting theory "Padic_Field.Padic_Semialgebraic_Function_Ring"
13:30:03Presenting theory "HOL-Analysis.Radon_Nikodym"
13:30:04Presenting theory "BenOr_Kozen_Reif.Renegar_Proofs"
13:30:04Presenting theory "HOL-Analysis.Set_Integral"
13:30:05Presenting theory "BenOr_Kozen_Reif.BKR_Decision"
13:30:05Presenting theory "HOL-Analysis.Homeomorphism"
13:30:05Presenting theory "BenOr_Kozen_Reif.Renegar_Decision"
13:30:06Presenting theory "Quantifier_Elimination_Hybrid.Renegar_Modified"
13:30:07Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Matrix_Proofs"
13:30:07Presenting theory "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
13:30:08Presenting theory "Quantifier_Elimination_Hybrid.Hybrid_Multiv_Algorithm_Proofs"
13:30:08Presenting theory "HOL-Analysis.Harmonic_Numbers"
13:30:09Presenting theory "HOL-Analysis.Gamma_Function"
13:30:10Presenting theory "HOL-Analysis.Interval_Integral"
13:30:11Presenting theory "HOL-Analysis.Lebesgue_Integral_Substitution"
13:30:11Presenting theory "HOL-Analysis.Ball_Volume"
13:30:11Presenting theory "HOL-Analysis.Integral_Test"
13:30:11Presenting theory "HOL-Analysis.Improper_Integral"
13:30:12Presenting theory "HOL-Analysis.Continuous_Extension"
13:30:12Presenting theory "HOL-Analysis.Equivalence_Measurable_On_Borel"
13:30:13Presenting theory "HOL-Analysis.Embed_Measure"
13:30:13Presenting theory "HOL-Analysis.Brouwer_Fixpoint"
13:30:14Presenting theory "HOL-Analysis.Fashoda_Theorem"
13:30:14Presenting theory "HOL-Analysis.Cross3"
13:30:14Presenting theory "HOL-Analysis.Bounded_Continuous_Function"
13:30:14Presenting theory "HOL-Analysis.Infinite_Products"
13:30:15Presenting theory "HOL-Analysis.Infinite_Set_Sum"
13:30:16Presenting theory "HOL-Analysis.Polytope"
13:30:17Presenting theory "HOL-Analysis.Retracts"
13:30:18Presenting theory "HOL-Analysis.Further_Topology"
13:30:20Presenting theory "HOL-Analysis.Jordan_Curve"
13:30:20Presenting theory "HOL-Analysis.Poly_Roots"
13:30:20Presenting theory "HOL-Analysis.Generalised_Binomial_Theorem"
13:30:20Presenting theory "HOL-Analysis.Vitali_Covering_Theorem"
13:30:22Presenting theory "HOL-Analysis.Change_Of_Vars"
13:30:22Presenting theory "HOL-Analysis.Lipschitz"
13:30:23Presenting theory "HOL-Analysis.Multivariate_Analysis"
13:30:23Presenting theory "HOL-Analysis.Simplex_Content"
13:30:23Presenting theory "HOL-Analysis.FPS_Convergence"
13:30:23Presenting theory "HOL-Analysis.Smooth_Paths"
13:30:23Presenting theory "HOL-Analysis.Function_Metric"
13:30:24Presenting theory "HOL-Analysis.Analysis"
13:30:24Presenting theory "HOL-Probability.Probability_Measure"
13:30:25Presenting theory "HOL-Probability.Giry_Monad"
13:30:25Presenting theory "HOL-Probability.Probability_Mass_Function"
13:30:26Presenting theory "Finite_Fields.Finite_Fields_More_PMF"
13:30:26Presenting theory "Finite_Fields.Finite_Fields_Poly_Factor_Ring_Code"
13:30:26Presenting theory "HOL-Probability.Distribution_Functions"
13:30:26Presenting theory "HOL-Probability.Weak_Convergence"
13:30:27Presenting theory "HOL-Probability.Projective_Family"
13:30:27Presenting theory "HOL-Probability.Infinite_Product_Measure"
13:30:27Presenting theory "HOL-Probability.Independent_Family"
13:30:28Presenting theory "HOL-Probability.Convolution"
13:30:28Presenting theory "HOL-Probability.Information"
13:30:29Presenting theory "HOL-Probability.Distributions"
13:30:30Presenting theory "HOL-Probability.Characteristic_Functions"
13:30:30Presenting theory "HOL-Probability.Helly_Selection"
13:30:30Presenting theory "HOL-Probability.Sinc_Integral"
13:30:30Presenting theory "HOL-Probability.Levy"
13:30:30Presenting theory "HOL-Probability.Central_Limit_Theorem"
13:30:30Presenting theory "HOL-Probability.Discrete_Topology"
13:30:31Presenting theory "HOL-Probability.PMF_Impl"
13:30:31Presenting theory "HOL-Probability.Fin_Map"
13:30:31Presenting theory "HOL-Probability.Projective_Limit"
13:30:32Presenting theory "HOL-Combinatorics.Multiset_Permutations"
13:30:32Presenting theory "HOL-Probability.Random_Permutations"
13:30:32Presenting theory "HOL-Probability.SPMF"
13:30:33Presenting theory "HOL-Probability.Product_PMF"
13:30:33Presenting theory "HOL-Probability.Hoeffding"
13:30:34Presenting theory "HOL-Probability.Stream_Space"
13:30:34Presenting theory "HOL-Probability.Tree_Space"
13:30:35Presenting theory "HOL-Probability.Conditional_Expectation"
13:30:35Presenting theory "HOL-Probability.Essential_Supremum"
13:30:35Presenting theory "HOL-Probability.Stopping_Time"
13:30:35Presenting theory "HOL-Probability.Probability"
13:30:35Presenting theory "MFMC_Countable.MFMC_Misc"
13:30:35Presenting theory "Flow_Networks.Graph"
13:30:35Presenting theory "Flow_Networks.Network"
13:30:35Presenting theory "Flow_Networks.Residual_Graph"
13:30:35Presenting theory "Flow_Networks.Augmenting_Flow"
13:30:36Presenting theory "Flow_Networks.Augmenting_Path"
13:30:36Presenting theory "Flow_Networks.Ford_Fulkerson"
13:30:36Presenting theory "EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract"
13:30:36Presenting theory "MFMC_Countable.MFMC_Finite"
13:30:36Presenting theory "MFMC_Countable.Matrix_For_Marginals"
13:30:36Presenting theory "MFMC_Countable.Rel_PMF_Characterisation"
13:30:36Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
13:30:36Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
13:30:36Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
13:30:36Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
13:30:36Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
13:30:36Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
13:30:36Presenting theory "Probabilistic_While.While_SPMF"
13:30:37Presenting theory "Executable_Randomized_Algorithms.Coin_Space"
13:30:37Presenting theory "Executable_Randomized_Algorithms.Tau_Additivity"
13:30:37Presenting theory "HOL-Complex_Analysis.Contour_Integration"
13:30:38Presenting theory "HOL-Complex_Analysis.Cauchy_Integral_Theorem"
13:30:39Presenting theory "HOL-Complex_Analysis.Winding_Numbers"
13:30:40Presenting theory "HOL-Complex_Analysis.Cauchy_Integral_Formula"
13:30:41Presenting theory "HOL-Complex_Analysis.Conformal_Mappings"
13:30:42Presenting theory "HOL-Complex_Analysis.Great_Picard"
13:30:43Presenting theory "HOL-Complex_Analysis.Riemann_Mapping"
13:30:43Presenting theory "HOL-Complex_Analysis.Complex_Singularities"
13:30:44Presenting theory "HOL-Complex_Analysis.Complex_Residues"
13:30:44Presenting theory "HOL-Complex_Analysis.Residue_Theorem"
13:30:45Presenting theory "HOL-Complex_Analysis.Laurent_Convergence"
13:30:46Presenting theory "HOL-Complex_Analysis.Meromorphic"
13:30:46Presenting theory "HOL-Complex_Analysis.Weierstrass_Factorization"
13:30:46Presenting theory "HOL-Complex_Analysis.Complex_Analysis"
13:30:46Presenting theory "Dirichlet_Series.More_Totient"
13:30:46Presenting theory "Dirichlet_Series.Liouville_Lambda"
13:30:46Presenting theory "Dirichlet_Series.Divisor_Count"
13:30:47Presenting theory "Dirichlet_Series.Arithmetic_Summatory"
13:30:47Presenting theory "Dirichlet_Series.Partial_Summation"
13:30:47Presenting theory "Dirichlet_Series.Euler_Products"
13:30:47Presenting theory "Dirichlet_Series.Dirichlet_Series_Analysis"
13:30:48Presenting theory "Zeta_Function.Zeta_Library"
13:30:48Presenting theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal"
13:30:49Presenting theory "Executable_Randomized_Algorithms.Randomized_Algorithm"
13:30:49Presenting theory "Finite_Fields.Find_Irreducible_Poly"
13:30:49Unfinished session(s): Approximate_Model_Counting, Frequency_Moments
13:30:4913:30:49=== TIMING ===
13:30:4913:30:49Group AFP: 5:35:35 elapsed time, 20:35:16 cpu time, factor 3.68
13:30:49Group main: 0:08:03 elapsed time, 0:19:47 cpu time, factor 2.46
13:30:49Group large: 0:00:00 elapsed time
13:30:49Group no_doc: 0:00:00 elapsed time
13:30:49Group doc: 0:00:00 elapsed time
13:30:49Group timing: 0:20:50 elapsed time, 1:18:01 cpu time, factor 3.74
13:30:49Overall: 1:10:34 elapsed time, 21:53:18 cpu time, factor 18.61
13:30:4913:30:49=== FAILED SESSIONS ===
13:30:4913:30:49Session Frequency_Moments: FAILED 142
13:30:49Session Approximate_Model_Counting: CANCELLED
13:30:5313:30:53=== REPORT ===
13:30:5313:30:53Writing report file ...
13:30:5313:30:53=== SITEGEN ===
13:30:5313:30:53Writing status file ...
13:30:53Running sitegen ...
13:30:53using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
13:30:55Preparing site generation in out/hugo
13:30:55Cleaning up generated files...
13:30:55Preparing topics...
13:30:55Preparing licenses...
13:30:55Preparing releases...
13:30:56Preparing authors...
13:31:00Extracting keywords...
13:31:01Preparing entries...
13:31:49### No DOI cache found - resolving might take some time
13:35:45Preparing statistics...
13:35:50Preparing project files
13:35:50Preparing devel version...
13:35:50Finished sitegen preparation.
13:35:50Cleaning output dir...
13:35:51Building site...
13:35:55Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
13:35:55Packing tars ...
13:36:1713:36:17=== NOTIFICATIONS ===
13:36:1713:36:1813:36:18=== COMPLETED ===
13:36:1813:36:19Build step 'Execute shell' marked build as failure
13:40:48Started calculate disk usage of build
13:40:48Finished Calculation of disk usage of build in 0 seconds
13:40:48Started calculate disk usage of workspace
13:40:49Finished Calculation of disk usage of workspace in 1 second
13:40:50Email was triggered for: Failure - 1st
13:40:50Trigger Failure - Any was overridden by another trigger and will not send an email.
13:40:50Trigger Failure - Still was overridden by another trigger and will not send an email.
13:40:50Sending email for trigger: Failure - 1st
13:40:50Sending email to: isabelle-ci@mailman46.in.tum.de
13:40:50Finished: FAILURE
![[Jenkins]](/jenkins/static/51af4dc4/images/svgs/logo.svg){kind=logo}
