Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. merge
  2. merge from AFP Isabelle2017, already adapted Treaps, First_Order_Terms, LLL_Basis_Reduction
  3. adjusted sequence of author's in Treaps (accord. to mail by Manuel), typo in abstract of First_Order_Terms
  4. New entry LLL_Factorization
  5. website update
  6. new entry: Treaps
  7. New entry: First_Order_Terms
  8. new entry LLL_Basis_Reduction
Changeset 8875:7ae2c8867e11 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 8874:579fc2d81a17 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge from AFP Isabelle2017, already adapted Treaps, First_Order_Terms, LLL_Basis_Reduction
Changeset 8873:0ef5cc63aa30 by rene thiemann _rene.thiemann@uibk.ac.at_:
adjusted sequence of author's in Treaps (accord. to mail by Manuel), typo in abstract of First_Order_Terms
The file was modified metadata/metadata (diff)
The file was modified thys/First_Order_Terms/document/root.tex (diff)
The file was modified web/entries/First_Order_Terms.html (diff)
The file was modified web/entries/Treaps.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
Changeset 8872:8be0d32f2c6d by nipkow:
New entry LLL_Factorization
The file was addedthys/LLL_Factorization/Factor_Bound_2.thy
The file was addedthys/LLL_Factorization/Factorization_Algorithm_16_22.thy
The file was addedthys/LLL_Factorization/LLL_Factorization.thy
The file was addedthys/LLL_Factorization/LLL_Factorization_Impl.thy
The file was addedthys/LLL_Factorization/Missing_Dvd_Int_Poly.thy
The file was addedthys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy
The file was addedthys/LLL_Factorization/ROOT
The file was addedthys/LLL_Factorization/document/root.bib
The file was addedthys/LLL_Factorization/document/root.tex
The file was addedweb/entries/LLL_Factorization.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Algebraic_Numbers.html (diff)
The file was modified web/entries/Berlekamp_Zassenhaus.html (diff)
The file was modified web/entries/Jordan_Normal_Form.html (diff)
The file was modified web/entries/LLL_Basis_Reduction.html (diff)
The file was modified web/entries/Perron_Frobenius.html (diff)
The file was modified web/entries/Polynomial_Factorization.html (diff)
The file was modified web/entries/Polynomial_Interpolation.html (diff)
The file was modified web/entries/Subresultants.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 8871:32cd532772c1 by rene thiemann _rene.thiemann@uibk.ac.at_:
website update
The file was addedweb/entries/Treaps.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/AVL-Trees.html (diff)
The file was modified web/entries/Abs_Int_ITP2012.html (diff)
The file was modified web/entries/Abstract-Hoare-Logics.html (diff)
The file was modified web/entries/Akra_Bazzi.html (diff)
The file was modified web/entries/Amortized_Complexity.html (diff)
The file was modified web/entries/ArrowImpossibilityGS.html (diff)
The file was modified web/entries/Bernoulli.html (diff)
The file was modified web/entries/Bertrands_Postulate.html (diff)
The file was modified web/entries/Boolean_Expression_Checkers.html (diff)
The file was modified web/entries/Buffons_Needle.html (diff)
The file was modified web/entries/CAVA_LTL_Modelchecker.html (diff)
The file was modified web/entries/Catalan_Numbers.html (diff)
The file was modified web/entries/Comparison_Sort_Lower_Bound.html (diff)
The file was modified web/entries/Compiling-Exceptions-Correctly.html (diff)
The file was modified web/entries/Density_Compiler.html (diff)
The file was modified web/entries/Descartes_Sign_Rule.html (diff)
The file was modified web/entries/Dirichlet_Series.html (diff)
The file was modified web/entries/Dynamic_Tables.html (diff)
The file was modified web/entries/E_Transcendental.html (diff)
The file was modified web/entries/Euler_MacLaurin.html (diff)
The file was modified web/entries/Fisher_Yates.html (diff)
The file was modified web/entries/Flyspeck-Tame.html (diff)
The file was modified web/entries/FunWithFunctions.html (diff)
The file was modified web/entries/FunWithTilings.html (diff)
The file was modified web/entries/Functional-Automata.html (diff)
The file was modified web/entries/Gauss-Jordan-Elim-Fun.html (diff)
The file was modified web/entries/HotelKeyCards.html (diff)
The file was modified web/entries/Jinja.html (diff)
The file was modified web/entries/Landau_Symbols.html (diff)
The file was modified web/entries/LinearQuantifierElim.html (diff)
The file was modified web/entries/Linear_Recurrences.html (diff)
The file was modified web/entries/Liouville_Numbers.html (diff)
The file was modified web/entries/List-Index.html (diff)
The file was modified web/entries/List_Update.html (diff)
The file was modified web/entries/MSO_Regex_Equivalence.html (diff)
The file was modified web/entries/Markov_Models.html (diff)
The file was modified web/entries/Marriage.html (diff)
The file was modified web/entries/Mason_Stothers.html (diff)
The file was modified web/entries/Median_Of_Medians_Selection.html (diff)
The file was modified web/entries/MiniML.html (diff)
The file was modified web/entries/Minkowskis_Theorem.html (diff)
The file was modified web/entries/Monad_Normalisation.html (diff)
The file was modified web/entries/NormByEval.html (diff)
The file was modified web/entries/Pairing_Heap.html (diff)
The file was modified web/entries/Prime_Harmonic_Series.html (diff)
The file was modified web/entries/Priority_Queue_Braun.html (diff)
The file was modified web/entries/Propositional_Proof_Systems.html (diff)
The file was modified web/entries/Quick_Sort_Cost.html (diff)
The file was modified web/entries/Random_BSTs.html (diff)
The file was modified web/entries/Randomised_Social_Choice.html (diff)
The file was modified web/entries/Regex_Equivalence.html (diff)
The file was modified web/entries/Regular-Sets.html (diff)
The file was modified web/entries/Root_Balanced_Tree.html (diff)
The file was modified web/entries/SDS_Impossibility.html (diff)
The file was modified web/entries/Simple_Firewall.html (diff)
The file was modified web/entries/Skew_Heap.html (diff)
The file was modified web/entries/Splay_Tree.html (diff)
The file was modified web/entries/Stirling_Formula.html (diff)
The file was modified web/entries/Sturm_Sequences.html (diff)
The file was modified web/entries/Triangle.html (diff)
The file was modified web/entries/Trie.html (diff)
The file was modified web/entries/Zeta_Function.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 8870:ba0751534695 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Treaps
The file was addedthys/Treaps/Probability_Misc.thy
The file was addedthys/Treaps/ROOT
The file was addedthys/Treaps/Random_List_Permutation.thy
The file was addedthys/Treaps/Random_Treap.thy
The file was addedthys/Treaps/Treap.thy
The file was addedthys/Treaps/Treap_Sort_and_BSTs.thy
The file was addedthys/Treaps/document/root.bib
The file was addedthys/Treaps/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8869:26905d636473 by nipkow:
New entry: First_Order_Terms
The file was addedthys/First_Order_Terms/Abstract_Unification.thy
The file was addedthys/First_Order_Terms/Fun_More.thy
The file was addedthys/First_Order_Terms/Option_Monad.thy
The file was addedthys/First_Order_Terms/ROOT
The file was addedthys/First_Order_Terms/Seq_More.thy
The file was addedthys/First_Order_Terms/Subsumption.thy
The file was addedthys/First_Order_Terms/Term.thy
The file was addedthys/First_Order_Terms/Term_Pair_Multiset.thy
The file was addedthys/First_Order_Terms/Transitive_Closure_More.thy
The file was addedthys/First_Order_Terms/Unification.thy
The file was addedthys/First_Order_Terms/Unifiers.thy
The file was addedthys/First_Order_Terms/document/root.bib
The file was addedthys/First_Order_Terms/document/root.tex
The file was addedweb/entries/First_Order_Terms.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Abstract-Rewriting.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 8868:4356cf854519 by nipkow:
new entry LLL_Basis_Reduction
The file was addedthys/LLL_Basis_Reduction/Gram_Schmidt_2.thy
The file was addedthys/LLL_Basis_Reduction/LLL.thy
The file was addedthys/LLL_Basis_Reduction/List_Representation.thy
The file was addedthys/LLL_Basis_Reduction/Missing_Lemmas.thy
The file was addedthys/LLL_Basis_Reduction/Norms.thy
The file was addedthys/LLL_Basis_Reduction/ROOT
The file was addedthys/LLL_Basis_Reduction/Vector_Lattice_Locale.thy
The file was addedthys/LLL_Basis_Reduction/document/root.bib
The file was addedthys/LLL_Basis_Reduction/document/root.tex
The file was addedweb/entries/LLL_Basis_Reduction.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Abstract-Rewriting.html (diff)
The file was modified web/entries/Algebraic_Numbers.html (diff)
The file was modified web/entries/Berlekamp_Zassenhaus.html (diff)
The file was modified web/entries/Certification_Monads.html (diff)
The file was modified web/entries/Datatype_Order_Generator.html (diff)
The file was modified web/entries/Deriving.html (diff)
The file was modified web/entries/Echelon_Form.html (diff)
The file was modified web/entries/Gauss_Jordan.html (diff)
The file was modified web/entries/Hermite.html (diff)
The file was modified web/entries/Jordan_Normal_Form.html (diff)
The file was modified web/entries/Lifting_Definition_Option.html (diff)
The file was modified web/entries/Matrix.html (diff)
The file was modified web/entries/Partial_Function_MR.html (diff)
The file was modified web/entries/Perron_Frobenius.html (diff)
The file was modified web/entries/Polynomial_Factorization.html (diff)
The file was modified web/entries/Polynomial_Interpolation.html (diff)
The file was modified web/entries/Polynomials.html (diff)
The file was modified web/entries/QR_Decomposition.html (diff)
The file was modified web/entries/Rank_Nullity_Theorem.html (diff)
The file was modified web/entries/Real_Impl.html (diff)
The file was modified web/entries/Show.html (diff)
The file was modified web/entries/Sqrt_Babylonian.html (diff)
The file was modified web/entries/Stochastic_Matrices.html (diff)
The file was modified web/entries/Subresultants.html (diff)
The file was modified web/entries/Transitive-Closure-II.html (diff)
The file was modified web/entries/Transitive-Closure.html (diff)
The file was modified web/entries/XML.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)