Talk on Export of formal theory content

On 22-Nov-2019 I have delivered the following talk at TUM (Garching bei M√ľnchen):

Title:
Export of formal theory content in Isabelle/Scala
Abstract:
This is an overview of the state of affairs of systematic export of formal theory content. The general motivation is to provide semantically enriched views on the Isabelle/AFP library, without requiring a running Isabelle process. A typical application could be search over a database of digested theories, e.g. for an AFP web service.
Materials:
Slides with sources, which include practically relevant links and examples.