Skip to content
Success

Changes

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

Summary

  1. merge from afp-2021-1
  2. tuned;
  3. tooling: added utility to check for metadata consistency;
  4. regenerate website;
  5. site: generate multi-line json for smaller merges;
  6. toml module: proper parsing of quotes in multiline strings;
  7. added further sitegen generated websites
  8. added metadata for Real_Time_Deque's, sitegen
  9. new entry: Real-Time Double-Ended Queue
Changeset 12763:2c63017ece34 by fabian huch _huch@in.tum.de_:
merge from afp-2021-1
The file was modified tools/afp_check_metadata.scala
Changeset 12761:040f15ef87ce by fabian huch _huch@in.tum.de_:
tooling: added utility to check for metadata consistency;
The file was addedtools/afp_check_metadata.scala
The file was modified etc/build.props
The file was modified tools/afp_tool.scala
Changeset 12760:a892193d066e by fabian huch _huch@in.tum.de_:
regenerate website;
The file was modified web/data/keywords.json
The file was modified web/entries/Real_Time_Deque.html
The file was modified web/index.json
Changeset 12759:9611eb049619 by fabian huch _huch@in.tum.de_:
site: generate multi-line json for smaller merges;
The file was modified admin/site/themes/afp/layouts/_default/index.json
The file was modified tools/hugo.scala
Changeset 12758:3835b6036d7d by fabian huch _huch@in.tum.de_:
toml module: proper parsing of quotes in multiline strings;
The file was modified tools/toml.scala
Changeset 12757:fe0311217631 by rene thiemann _rene.thiemann@uibk.ac.at_:
added further sitegen generated websites
The file was addedweb/entries/Real_Time_Deque.html
The file was addedweb/theories/real_time_deque/index.html
Changeset 12756:cff33f5834e6 by rene thiemann _rene.thiemann@uibk.ac.at_:
added metadata for Real_Time_Deque's, sitegen
The file was addedmetadata/entries/Real_Time_Deque.toml
The file was addedweb/authors/toth/index.html
The file was addedweb/authors/toth/index.xml
The file was modified metadata/authors.toml
The file was modified thys/Real_Time_Deque/ROOT
The file was modified web/authors/index.html
The file was modified web/authors/index.json
The file was modified web/authors/nipkow/index.html
The file was modified web/authors/nipkow/index.xml
The file was modified web/data/keywords.json
The file was modified web/entries/index.html
The file was modified web/entries/index.xml
The file was modified web/index.html
The file was modified web/index.json
The file was modified web/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/theories/index.xml
The file was modified web/topics/computer-science/data-structures/index.html
The file was modified web/topics/computer-science/data-structures/index.xml
The file was modified web/topics/index.html
Changeset 12755:27a40bfc433a by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Real-Time Double-Ended Queue
The file was addedthys/Real_Time_Deque/Big.thy
The file was addedthys/Real_Time_Deque/Big_Proof.thy
The file was addedthys/Real_Time_Deque/Common.thy
The file was addedthys/Real_Time_Deque/Common_Proof.thy
The file was addedthys/Real_Time_Deque/Current.thy
The file was addedthys/Real_Time_Deque/Current_Proof.thy
The file was addedthys/Real_Time_Deque/Deque.thy
The file was addedthys/Real_Time_Deque/Idle.thy
The file was addedthys/Real_Time_Deque/Idle_Proof.thy
The file was addedthys/Real_Time_Deque/ROOT
The file was addedthys/Real_Time_Deque/RTD_Util.thy
The file was addedthys/Real_Time_Deque/RealTimeDeque.thy
The file was addedthys/Real_Time_Deque/RealTimeDeque_Dequeue.thy
The file was addedthys/Real_Time_Deque/RealTimeDeque_Enqueue.thy
The file was addedthys/Real_Time_Deque/RealTimeDeque_Proof.thy
The file was addedthys/Real_Time_Deque/Small.thy
The file was addedthys/Real_Time_Deque/Small_Proof.thy
The file was addedthys/Real_Time_Deque/Stack.thy
The file was addedthys/Real_Time_Deque/Stack_Proof.thy
The file was addedthys/Real_Time_Deque/States.thy
The file was addedthys/Real_Time_Deque/States_Proof.thy
The file was addedthys/Real_Time_Deque/Type_Classes.thy
The file was addedthys/Real_Time_Deque/document/root.bib
The file was addedthys/Real_Time_Deque/document/root.tex
The file was modified thys/ROOTS