Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merge from afp-2017
  2. new entry: Kuratowski_Closure_Complement
  3. tweaks to example submission for Isabelle2017
  4. new entries: Transition_Systems_and_Automata and Buchi_Complementation
  5. documented change policy
  6. more doc by Lars Hupel
  7. added missing file from Diophantine_Eqns_Lin_Hom (warning appears at every Isabelle/jedit start)
  8. merge
  9. compatability patch for Perron-Frobenius (old version is not compatible with Gabow_SCC)
  10. website for Count-Complex-Roots
  11. new entry Count-Complex-Roots by Wenda Li
  12. website for Winding Number
  13. new entry: Winding Number Eval by Wenda Li
  14. Linear_Recurrences website
  15. new submission Linear_Recurrences
  16. website for Zeta_Function
  17. new entry Zeta_Function
  18. website for Dirichlet_Series
  19. new entry Dirichlet_Series
  20. website for Lowe_Ontological_Argument
  21. merged
  22. metadata for Lowe_Ontological_Argument
  23. new entry Lowe_Ontological_Argument
  24. new entry Diophantine_Eqns_Lin_Hom
  25. fix by Lars
Changeset 8491:22dedea5ab5d by kleing:
merge from afp-2017
Changeset 8490:af339feda8de by gerwin.klein@data61.csiro.au:
new entry: Kuratowski_Closure_Complement
The file was addedthys/Kuratowski_Closure_Complement/KuratowskiClosureComplementTheorem.thy
The file was addedthys/Kuratowski_Closure_Complement/ROOT
The file was addedthys/Kuratowski_Closure_Complement/document/root.bib
The file was addedthys/Kuratowski_Closure_Complement/document/root.tex
The file was addedweb/entries/Kuratowski_Closure_Complement.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/ConcurrentGC.html (diff)
The file was modified web/entries/ConcurrentIMP.html (diff)
The file was modified web/entries/KBPs.html (diff)
The file was modified web/entries/PCF.html (diff)
The file was modified web/entries/SenSocialChoice.html (diff)
The file was modified web/entries/Stable_Matching.html (diff)
The file was modified web/entries/Stern_Brocot.html (diff)
The file was modified web/entries/TortoiseHare.html (diff)
The file was modified web/entries/WorkerWrapper.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 8489:c9cbfb56b64b by gerwin.klein@data61.csiro.au:
tweaks to example submission for Isabelle2017
The file was modified thys/Example-Submission/Submission.thy (diff)
Changeset 8488:8711e4eaa550 by gerwin.klein@data61.csiro.au:
new entries: Transition_Systems_and_Automata and Buchi_Complementation
The file was addedthys/Buchi_Complementation/Alternate.thy
The file was addedthys/Buchi_Complementation/Complementation.thy
The file was addedthys/Buchi_Complementation/Complementation_Implement.thy
The file was addedthys/Buchi_Complementation/Graph.thy
The file was addedthys/Buchi_Complementation/ROOT
The file was addedthys/Buchi_Complementation/Ranking.thy
The file was addedthys/Buchi_Complementation/document/root.bib
The file was addedthys/Buchi_Complementation/document/root.tex
The file was addedthys/Transition_Systems_and_Automata/Automata/BA.thy
The file was addedthys/Transition_Systems_and_Automata/Automata/BA_Implement.thy
The file was addedthys/Transition_Systems_and_Automata/Automata/BA_Refine.thy
The file was addedthys/Transition_Systems_and_Automata/Automata/DFA.thy
The file was addedthys/Transition_Systems_and_Automata/Automata/NFA.thy
The file was addedthys/Transition_Systems_and_Automata/Basic/Basic.thy
The file was addedthys/Transition_Systems_and_Automata/Basic/Implement.thy
The file was addedthys/Transition_Systems_and_Automata/Basic/Refine.thy
The file was addedthys/Transition_Systems_and_Automata/Basic/Sequence.thy
The file was addedthys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy
The file was addedthys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy
The file was addedthys/Transition_Systems_and_Automata/ROOT
The file was addedthys/Transition_Systems_and_Automata/Transition_Systems/Transition_System.thy
The file was addedthys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Construction.thy
The file was addedthys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Extra.thy
The file was addedthys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Refine.thy
The file was addedthys/Transition_Systems_and_Automata/document/root.tex
The file was addedweb/entries/Buchi_Complementation.html
The file was addedweb/entries/Transition_Systems_and_Automata.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Collections.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 8487:4bbae4bf607c by nipkow:
documented change policy
The file was modified admin/sitegen-lib/templates/updating.tpl (diff)
The file was modified web/updating.html (diff)
Changeset 8486:991bee954bad by nipkow:
more doc by Lars Hupel
The file was addeddoc/editors/web.md
The file was modified metadata/README (diff)
Changeset 8485:3bd81cd4f2c9 by rene thiemann _rene.thiemann@uibk.ac.at_:
added missing file from Diophantine_Eqns_Lin_Hom (warning appears at every Isabelle/jedit start)
The file was addedthys/Diophantine_Eqns_Lin_Hom/src/Main.hs
Changeset 8484:bc9311a8bac7 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 8483:512e25c745f3 by rene thiemann _rene.thiemann@uibk.ac.at_:
compatability patch for Perron-Frobenius (old version is not compatible with Gabow_SCC)
The file was addedthys/Perron_Frobenius/Check_Matrix_Growth.thy
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_General.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy (diff)
The file was modified thys/Perron_Frobenius/ROOT (diff)
The file was modified thys/Perron_Frobenius/Spectral_Radius_Theory_2.thy (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/Graph_Theory.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/Rank_Nullity_Theorem.html (diff)
The file was modified web/statistics.html (diff)
Changeset 8482:8ab9e521854a by rene thiemann _rene.thiemann@uibk.ac.at_:
website for Count-Complex-Roots
The file was addedweb/entries/Count_Complex_Roots.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Sturm_Tarski.html (diff)
The file was modified web/entries/Winding_Number_Eval.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 8481:dba863a1ab65 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry Count-Complex-Roots by Wenda Li
The file was addedthys/Count_Complex_Roots/Count_Complex_Roots.thy
The file was addedthys/Count_Complex_Roots/Count_Complex_Roots_Examples.thy
The file was addedthys/Count_Complex_Roots/Extended_Sturm.thy
The file was addedthys/Count_Complex_Roots/ROOT
The file was addedthys/Count_Complex_Roots/document/root.bib
The file was addedthys/Count_Complex_Roots/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8480:2ed5a403ca81 by rene thiemann _rene.thiemann@uibk.ac.at_:
website for Winding Number
The file was addedweb/entries/Winding_Number_Eval.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Koenigsberg_Friendship.html (diff)
The file was modified web/entries/Sturm_Tarski.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 8479:f65adca7c8a1 by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Winding Number Eval by Wenda Li
The file was addedthys/Winding_Number_Eval/Cauchy_Index_Theorem.thy
The file was addedthys/Winding_Number_Eval/Missing_Algebraic.thy
The file was addedthys/Winding_Number_Eval/Missing_Analysis.thy
The file was addedthys/Winding_Number_Eval/Missing_Topology.thy
The file was addedthys/Winding_Number_Eval/Missing_Transcendental.thy
The file was addedthys/Winding_Number_Eval/ROOT
The file was addedthys/Winding_Number_Eval/Winding_Number_Eval.thy
The file was addedthys/Winding_Number_Eval/Winding_Number_Eval_Examples.thy
The file was addedthys/Winding_Number_Eval/document/root.bib
The file was addedthys/Winding_Number_Eval/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8478:3e55f3bc279d by paulson _lp15@cam.ac.uk_:
Linear_Recurrences website
The file was addedweb/entries/Linear_Recurrences.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Algebraic_Numbers.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 8477:ad7be333896a by paulson _lp15@cam.ac.uk_:
new submission Linear_Recurrences
The file was addedthys/Linear_Recurrences/Eulerian_Polynomials.thy
The file was addedthys/Linear_Recurrences/Factorizations.thy
The file was addedthys/Linear_Recurrences/Linear_Homogenous_Recurrences.thy
The file was addedthys/Linear_Recurrences/Linear_Inhomogenous_Recurrences.thy
The file was addedthys/Linear_Recurrences/Linear_Recurrences_Common.thy
The file was addedthys/Linear_Recurrences/Linear_Recurrences_Misc.thy
The file was addedthys/Linear_Recurrences/Linear_Recurrences_Pretty.thy
The file was addedthys/Linear_Recurrences/Linear_Recurrences_Solver.thy
The file was addedthys/Linear_Recurrences/Linear_Recurrences_Test.thy
The file was addedthys/Linear_Recurrences/Partial_Fraction_Decomposition.thy
The file was addedthys/Linear_Recurrences/Pochhammer_Polynomials.thy
The file was addedthys/Linear_Recurrences/ROOT
The file was addedthys/Linear_Recurrences/RatFPS.thy
The file was addedthys/Linear_Recurrences/Rational_FPS_Solver.thy
The file was addedthys/Linear_Recurrences/Show_RatFPS.thy
The file was addedthys/Linear_Recurrences/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8476:4219882d5c46 by paulson _lp15@cam.ac.uk_:
website for Zeta_Function
The file was addedweb/entries/Zeta_Function.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Bernoulli.html (diff)
The file was modified web/entries/Dirichlet_Series.html (diff)
The file was modified web/entries/Euler_MacLaurin.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 8475:0cda00adf8e1 by paulson _lp15@cam.ac.uk_:
new entry Zeta_Function
The file was addedthys/Zeta_Function/ROOT
The file was addedthys/Zeta_Function/Zeta_Function.thy
The file was addedthys/Zeta_Function/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8474:38d3223d1b96 by paulson _lp15@cam.ac.uk_:
website for Dirichlet_Series
The file was addedweb/entries/Dirichlet_Series.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Euler_MacLaurin.html (diff)
The file was modified web/entries/Landau_Symbols.html (diff)
The file was modified web/entries/Polynomial_Factorization.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 8473:e0acac066008 by paulson _lp15@cam.ac.uk_:
new entry Dirichlet_Series
The file was addedthys/Dirichlet_Series/Arithmetic_Summatory.thy
The file was addedthys/Dirichlet_Series/Arithmetic_Summatory_Asymptotics.thy
The file was addedthys/Dirichlet_Series/Dirichlet_Efficient_Code.thy
The file was addedthys/Dirichlet_Series/Dirichlet_Misc.thy
The file was addedthys/Dirichlet_Series/Dirichlet_Product.thy
The file was addedthys/Dirichlet_Series/Dirichlet_Series.thy
The file was addedthys/Dirichlet_Series/Dirichlet_Series_Analysis.thy
The file was addedthys/Dirichlet_Series/Divisor_Count.thy
The file was addedthys/Dirichlet_Series/Euler_Products.thy
The file was addedthys/Dirichlet_Series/Liouville_Lambda.thy
The file was addedthys/Dirichlet_Series/Moebius_Mu.thy
The file was addedthys/Dirichlet_Series/More_Totient.thy
The file was addedthys/Dirichlet_Series/Multiplicative_Function.thy
The file was addedthys/Dirichlet_Series/Partial_Summation.thy
The file was addedthys/Dirichlet_Series/ROOT
The file was addedthys/Dirichlet_Series/document/root.bib
The file was addedthys/Dirichlet_Series/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8472:a220a90858bb by paulson _lp15@cam.ac.uk_:
website for Lowe_Ontological_Argument
The file was addedweb/entries/Lowe_Ontological_Argument.html
The file was modified web/entries/GoedelGod.html (diff)
The file was modified web/entries/Types_Tableaus_and_Goedels_God.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 8471:241a340d337b by paulson:
merged
Changeset 8470:249023a44487 by paulson:
metadata for Lowe_Ontological_Argument
The file was modified metadata/metadata (diff)
Changeset 8469:2d7c18ba5007 by paulson:
new entry Lowe_Ontological_Argument
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_1.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_2.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_3.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_4.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_5.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_5b.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_6.thy
The file was addedthys/Lowe_Ontological_Argument/LoweOntologicalArgument_7.thy
The file was addedthys/Lowe_Ontological_Argument/QML.thy
The file was addedthys/Lowe_Ontological_Argument/ROOT
The file was addedthys/Lowe_Ontological_Argument/Relations.thy
The file was addedthys/Lowe_Ontological_Argument/document/root.bib
The file was addedthys/Lowe_Ontological_Argument/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 8468:52c04c8517d3 by nipkow:
new entry Diophantine_Eqns_Lin_Hom
The file was addedthys/Diophantine_Eqns_Lin_Hom/Algorithm.thy
The file was addedthys/Diophantine_Eqns_Lin_Hom/Linear_Diophantine_Equations.thy
The file was addedthys/Diophantine_Eqns_Lin_Hom/List_Vector.thy
The file was addedthys/Diophantine_Eqns_Lin_Hom/Makefile
The file was addedthys/Diophantine_Eqns_Lin_Hom/Minimize_Wrt.thy
The file was addedthys/Diophantine_Eqns_Lin_Hom/ROOT
The file was addedthys/Diophantine_Eqns_Lin_Hom/Solver_Code.thy
The file was addedthys/Diophantine_Eqns_Lin_Hom/Sorted_Wrt.thy
The file was addedthys/Diophantine_Eqns_Lin_Hom/document/root.bib
The file was addedthys/Diophantine_Eqns_Lin_Hom/document/root.tex
The file was addedweb/entries/Diophantine_Eqns_Lin_Hom.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (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 8467:9236f0d30c94 by nipkow:
fix by Lars
The file was modified admin/sitegen (diff)