Changes

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

polished theory
documented recent changes
documented changes in Show-entry
use new XML-transformer from IsaFoR, developed by A. Yamada
provide additional argument so that code-generation in SML/Eval does not fail
drop explicit injectivity proof, provide parsers for nat and int instead and derive injectivity

Changeset 14263:c60abfef602f by rene thiemann _rene.thiemann@uibk.ac.at_: polished theory
The file was modified	`thys/Show/Number_Parser.thy`
Changeset 14262:f5b7116751a9 by rene thiemann _rene.thiemann@uibk.ac.at_: documented recent changes
The file was modified	`metadata/entries/Berlekamp_Zassenhaus.toml`
The file was modified	`metadata/entries/Polynomial_Factorization.toml`
Changeset 14261:43c62567dc63 by rene thiemann _rene.thiemann@uibk.ac.at_: documented changes in Show-entry
The file was modified	`metadata/entries/Show.toml`
Changeset 14260:b086e875e09b by rene thiemann _rene.thiemann@uibk.ac.at_: use new XML-transformer from IsaFoR, developed by A. Yamada
The file was added	`thys/XML/Example_Application.thy`
The file was modified	`metadata/entries/XML.toml`
The file was modified	`thys/XML/ROOT`
The file was modified	`thys/XML/Xmlt.thy`
The file was modified	`thys/XML/document/root.tex`
Changeset 14259:b95e62c4c808 by rene thiemann _rene.thiemann@uibk.ac.at_: provide additional argument so that code-generation in SML/Eval does not fail
The file was modified	`thys/XML/Xml.thy`
Changeset 14258:8e2e746ba2c0 by rene thiemann _rene.thiemann@uibk.ac.at_: drop explicit injectivity proof, provide parsers for nat and int instead and derive injectivity
The file was added	`thys/Show/Number_Parser.thy`
The file was modified	`thys/Show/ROOT`
The file was modified	`thys/Show/Show_Instances.thy`