Skip to content
Failed

Changes

Summary

  1. regenerate website
  2. merge from afp-2016
  3. submission system only allows "../entry/thy" method
  4. tuned
  5. New entry Perron_Frobenius (and a few import tweaks of old theories)
  6. new entry Incredible_Proof_Machine
  7. capitalisation
  8. FLP webpage
  9. new entry FLP
  10. Randomised_Social_Choice: inserted timeout
  11. integrated improved equality test for algebraic numbers (unlike the previous algorithm, the new one terminates even if the factorization oracle delivers partial factorizations)
Changeset 6627:5b11db0303e0 by kleing:
regenerate website
The file was modified web/entries/LTL_to_DRA.shtml (diff)
Changeset 6626:55f42b8e820f by kleing:
merge from afp-2016
Changeset 6625:ed473f5b6a51 by gerwin.klein@nicta.com.au:
submission system only allows "../entry/thy" method
The file was modified web/using.shtml (diff)
Changeset 6624:ff1f8e03c75b by nipkow:
tuned
The file was modified metadata/metadata (diff)
The file was modified web/entries/Perron_Frobenius.shtml (diff)
Changeset 6623:479fddfc4c2a by nipkow:
New entry Perron_Frobenius (and a few import tweaks of old theories)
The file was addedthys/Jordan_Normal_Form/Gauss_Jordan_Elimination.thy
The file was addedthys/Perron_Frobenius/Bij_Nat.thy
The file was addedthys/Perron_Frobenius/Cancel_Card_Constraint.thy
The file was addedthys/Perron_Frobenius/Eigenvector_Homomorphism.thy
The file was addedthys/Perron_Frobenius/HMA_Connect.thy
The file was addedthys/Perron_Frobenius/Perron_Frobenius.thy
The file was addedthys/Perron_Frobenius/Perron_Frobenius_Aux.thy
The file was addedthys/Perron_Frobenius/ROOT
The file was addedthys/Perron_Frobenius/Spectral_Radius_Theory.thy
The file was addedthys/Perron_Frobenius/Square_Free_Factorization_Patched.thy
The file was addedthys/Perron_Frobenius/Types_To_Sets/Types_To_Sets.thy
The file was addedthys/Perron_Frobenius/Types_To_Sets/internalize_sort.ML
The file was addedthys/Perron_Frobenius/Types_To_Sets/local_typedef.ML
The file was addedthys/Perron_Frobenius/Types_To_Sets/unoverloading.ML
The file was addedthys/Perron_Frobenius/cancel_card_constraint.ML
The file was addedthys/Perron_Frobenius/document/root.bib
The file was addedthys/Perron_Frobenius/document/root.tex
The file was addedweb/entries/Perron_Frobenius.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/Cayley_Hamilton/Square_Matrix.thy (diff)
The file was modified thys/Jordan_Normal_Form/Column_Operations.thy (diff)
The file was modified thys/Jordan_Normal_Form/Gauss_Jordan_IArray_Impl.thy (diff)
The file was modified thys/Polynomial_Factorization/Gauss_Jordan_Field.thy (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
The file was removedthys/Jordan_Normal_Form/Gauss_Jordan.thy
Changeset 6622:835101fd5dff by nipkow:
new entry Incredible_Proof_Machine
The file was addedthys/Incredible_Proof_Machine/Abstract_Formula.thy
The file was addedthys/Incredible_Proof_Machine/Abstract_Rules.thy
The file was addedthys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy
The file was addedthys/Incredible_Proof_Machine/Build_Incredible_Tree.thy
The file was addedthys/Incredible_Proof_Machine/Entailment.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Completeness.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Correctness.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Deduction.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Everything.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Predicate.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Predicate_Tasks.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Propositional.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Propositional_Tasks.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Signatures.thy
The file was addedthys/Incredible_Proof_Machine/Incredible_Trees.thy
The file was addedthys/Incredible_Proof_Machine/Indexed_FSet.thy
The file was addedthys/Incredible_Proof_Machine/Inits.thy
The file was addedthys/Incredible_Proof_Machine/Natural_Deduction.thy
The file was addedthys/Incredible_Proof_Machine/Predicate_Formulas.thy
The file was addedthys/Incredible_Proof_Machine/Propositional_Formulas.thy
The file was addedthys/Incredible_Proof_Machine/ROOT
The file was addedthys/Incredible_Proof_Machine/Rose_Tree.thy
The file was addedthys/Incredible_Proof_Machine/Stream_Ext.thy
The file was addedthys/Incredible_Proof_Machine/document/root.bib
The file was addedthys/Incredible_Proof_Machine/document/root.tex
The file was addedweb/entries/Incredible_Proof_Machine.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 6621:3c977cab209c by paulson _lp15@cam.ac.uk_:
capitalisation
The file was modified metadata/metadata (diff)
The file was modified web/entries/FLP.shtml (diff)
The file was modified web/entries/MFMC_Countable.shtml (diff)
The file was modified web/index.shtml (diff)
Changeset 6620:1590284aa5ea by paulson _lp15@cam.ac.uk_:
FLP webpage
The file was addedweb/entries/FLP.shtml
The file was modified metadata/metadata (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 6619:ec4c351efc24 by paulson _lp15@cam.ac.uk_:
new entry FLP
The file was addedthys/FLP/AsynchronousSystem.thy
The file was addedthys/FLP/Execution.thy
The file was addedthys/FLP/FLPExistingSystem.thy
The file was addedthys/FLP/FLPSystem.thy
The file was addedthys/FLP/FLPTheorem.thy
The file was addedthys/FLP/ListUtilities.thy
The file was addedthys/FLP/Multiset.thy
The file was addedthys/FLP/ROOT
The file was addedthys/FLP/config
The file was addedthys/FLP/document/custom-macros.sty
The file was addedthys/FLP/document/root.bib
The file was addedthys/FLP/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 6618:45ac2355693c by paulson _lp15@cam.ac.uk_:
Randomised_Social_Choice: inserted timeout
The file was modified thys/Randomised_Social_Choice/ROOT (diff)
Changeset 6617:d72c4d0809a7 by rene thiemann _rene.thiemann@uibk.ac.at_:
integrated improved equality test for algebraic numbers<br>(unlike the previous algorithm, the new one terminates even if<br> the factorization oracle delivers partial factorizations)
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)