Parsing expanded

[dan323]

Adding more files to the isar2html2.0 parser

[dan323]

This an related changes are to parse theorems that state the output as obtains $vars where $props instead of only shows $props. Existential proofs.

[SKolodynski]

This looks like a useful addition. However, in the future let's discuss any additions to the syntax acceptable for isarmathlib.org beforehand. I am trying to keep the syntactic surface there as small as possible.

[dan323]

When I do a commit, it can be discussed. No need to just accept it.

[Copilot]

Pull request overview

This PR expands the isar2html2.0 pipeline to parse and render additional IsarMathLib theories, including support for proposition conclusions expressed with obtains ... where ..., and updates the published HTML docs accordingly.

Changes:

• Extend the F# parser/datamodel/exporter to represent proposition conclusions as either shows or obtains.
• Add additional theories to isar2html2.0/theories.conf so they are included in HTML generation.
• Update multiple Isabelle theory headers/proofs/text blocks and refresh generated HTML pages/index.

Reviewed changes

Copilot reviewed 24 out of 83 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
IsarMathLib/Ultrafilter_ZF.thy	Adds section intro text and refactors some proofs for ultrafilters.
IsarMathLib/Topology_ZF_9.thy	Improves explanatory text and refactors proof structure in homeomorphism-group results.
IsarMathLib/Topology_ZF_7.thy	Adds/edits narrative text and refactors some local proof steps in connection-properties theory.
IsarMathLib/Topology_ZF_10.thy	Clarifies product-topology narrative text and section introductions.
IsarMathLib/Ring_ZF_4.thy	Minor formatting/whitespace adjustments in ring lemmas/locales.
IsarMathLib/Ring_Zariski_ZF.thy	Adds structure/docs for spectrum/Zariski sections and switches Zariski ops to abbreviations; refactors proofs.
IsarMathLib/Ring_Zariski_ZF_1.thy	Adds subsection headings and narrative text for induced spectrum maps and continuity.
IsarMathLib/MetricUniform_ZF_1.thy	Names the DistWeight definition explicitly and formats it as a standard where definition.
isar2html2.0/theories.conf	Includes more theories in the HTML generation set.
isar2html2.0/src/isar2html/ProcessThys.fs	Propagates the new proposition “conclusion” representation into simplified items.
isar2html2.0/src/isar2html/IMLParser.fs	Parses obtains ... where ... conclusions; improves abbreviation notation parsing and adds safe tactic.
isar2html2.0/src/isar2html/IMLP_datatypes.fs	Introduces PropConclusion and updates proposition/simple-prop records accordingly.
isar2html2.0/src/isar2html/Export2Html.fs	Renders shows vs obtains conclusions in both theorem bodies and hover/summary boxes.
docs/IsarMathLib/VectorSpace_ZF.html	Regenerated HTML output reflecting parser/output changes.
docs/IsarMathLib/Ring_Zariski_ZF_2.html	Removes an outdated generated HTML page.
docs/IsarMathLib/NatGenIntEx_ZF.html	Regenerated HTML output reflecting parser/output changes.
docs/IsarMathLib/index.html	Updates the session title and the theory index list to match the new generated set.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[dan323]

@SKolodynski I can remove the docs update in a new commit.