Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. removal of needless hypothesis in hd_rev and last_rev
Changeset 73510:c526eb2c7ca0 by paulson _lp15@cam.ac.uk_:
removal of needless hypothesis in hd_rev and last_rev
The file was modified src/HOL/Computational_Algebra/Polynomial.thy
The file was modified src/HOL/List.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. Fixed a failing proof
  2. merged
  3. fixes for new hd_rev and last_rev
  4. merge from afp-2021
  5. Infix notation for the less_sets relation
  6. merged
  7. simplified a few proofs
  8. sitegen and metadata for Constructive_Cryptography_CM
  9. new entry Constructive_Cryptography_CM
Changeset 11706:74dd55b9ef33 by paulson _lp15@cam.ac.uk_:
Fixed a failing proof
The file was modified thys/Simple_Firewall/SimpleFw_Semantics.thy
Changeset 11705:dc35057aa54f by paulson:
merged
Changeset 11704:86e8a4b1fb58 by paulson _lp15@cam.ac.uk_:
fixes for new hd_rev and last_rev
The file was modified thys/DFS_Framework/Examples/DFS_Find_Path.thy
The file was modified thys/Flyspeck-Tame/FaceDivisionProps.thy
The file was modified thys/Native_Word/More_Bits_Int.thy
The file was modified thys/Simple_Firewall/Primitives/Iface.thy
The file was modified thys/Tree_Decomposition/Graph.thy
Changeset 11703:693ae1ce0d54 by gerwin klein _kleing@unsw.edu.au_:
merge from afp-2021
Changeset 11702:e928ad3a61c3 by paulson _lp15@cam.ac.uk_:
Infix notation for the less_sets relation
The file was modified thys/Nash_Williams/Nash_Extras.thy
The file was modified thys/Nash_Williams/Nash_Williams.thy
The file was modified thys/Ordinal_Partitions/Omega_Omega.thy
The file was modified thys/Ordinal_Partitions/Partitions.thy
Changeset 11701:ae4ec73674cd by paulson:
merged
Changeset 11700:a1f0a543602e by paulson _lp15@cam.ac.uk_:
simplified a few proofs
The file was modified thys/Nash_Williams/Nash_Williams.thy
Changeset 11699:92bb16b93fd2 by rene thiemann _rene.thiemann@uibk.ac.at_:
sitegen and metadata for Constructive_Cryptography_CM
The file was addedweb/entries/Constructive_Cryptography_CM.html
The file was modified metadata/metadata
The file was modified web/entries/Constructive_Cryptography.html
The file was modified web/entries/Game_Based_Crypto.html
The file was modified web/entries/Sigma_Commit_Crypto.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 11698:680fb435498b by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry Constructive_Cryptography_CM
The file was addedthys/Constructive_Cryptography_CM/Asymptotic_Security.thy
The file was addedthys/Constructive_Cryptography_CM/Concrete_Security.thy
The file was addedthys/Constructive_Cryptography_CM/Construction_Utility.thy
The file was addedthys/Constructive_Cryptography_CM/Constructions/DH_OTP.thy
The file was addedthys/Constructive_Cryptography_CM/Constructions/Diffie_Hellman_CC.thy
The file was addedthys/Constructive_Cryptography_CM/Constructions/One_Time_Pad.thy
The file was addedthys/Constructive_Cryptography_CM/Fold_Spmf.thy
The file was addedthys/Constructive_Cryptography_CM/Fused_Resource.thy
The file was addedthys/Constructive_Cryptography_CM/Goodies.thy
The file was addedthys/Constructive_Cryptography_CM/More_CC.thy
The file was addedthys/Constructive_Cryptography_CM/Observe_Failure.thy
The file was addedthys/Constructive_Cryptography_CM/ROOT
The file was addedthys/Constructive_Cryptography_CM/Specifications/Channel.thy
The file was addedthys/Constructive_Cryptography_CM/Specifications/Key.thy
The file was addedthys/Constructive_Cryptography_CM/State_Isomorphism.thy
The file was addedthys/Constructive_Cryptography_CM/document/root.bib
The file was addedthys/Constructive_Cryptography_CM/document/root.tex
The file was modified thys/ROOTS