English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This is an overview of the Isabelle technology behind the Archive of FormalProofs (AFP). Interactive development and quasi-interactive build jobs imposesignificant demands of scalability on the logic (usually Isabelle/HOL), onIsabelle/ML for mathematical tool implementation, and on Isabelle/Scala forphysical system integration --- all integrated in Isabelle/PIDE (the ProverIDE). Continuous growth of AFP has demanded continuous improvements of Isabelleperformance. This is a report on the situation in Isabelle2019 (June 2019),with notable add-ons like prover session exports and headless PIDE forautomated updates based on semantic information. An example application isIsabelle/MMT, which is able to turn all of Isabelle + AFP into OMDoc and RDFtriples, but it is straight-forward to reuse the Isabelle technology for otherapplications.

Isabelle technology for the Archive of Formal Proofs with application to MMT