[isabelle-dev] NEWS: updates on theory export

[Makarius]

*** System ***

* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
exported as well: this spans an overall dependency graph of internal
inferences; it might help to reconstruct the formal structure of theory
libraries. See also the module Export_Theory in Isabelle/Scala.


This refers to Isabelle/853947643971.

There is more ongoing work on the export, but this marks an important
stepping stone: people often come to me for such a formal dependency
graph wrt. the inference kernel (note that it omits non-logical
dependencies like notation or other declarations).

This now works, because I have disentangled the proof term
identification and naming schemes sufficiently well, to link derivations
to the fact name space in an authentic manner. (See also Global_Theory
and Thm_Deps in Isabelle/ML.)

Further consequences will follow soon as corollaries ...


	Makarius