adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

docs: use archive link for locale docs 

This link is stable over Isabelle releases and can be updated once
the repo switches over to the next release.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-12-21 12:48:44 +11:00 committed by Gerwin Klein
parent ce67a725f7
commit f33b02f3d0
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
docs/arch-split.md
View File

@ -76,8 +76,7 @@ end
All architecture-specific definitions should be placed in the Arch locale, with
an appropriate global_naming scheme (see below).
If you're not familiar with locales, you should read the [locale
tutorial](http://isabelle.in.tum.de/dist/Isabelle2021/doc/locales.pdf). The
If you're not familiar with locales, you should read the [locale tutorial]. The
`Arch` locale has no parameters and no assumptions, since we are merely using it
as a namespace, but it still important to understand the various ways of
interpreting this locale, how it interacts with various other locales in the
@ -88,6 +87,8 @@ because the generic theories need to be able to selectively refer to types,
constants and facts from architecture-specific theories, without naming a
particular architecture. The mechanisms for doing this are described below.
[locale tutorial]: https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021/doc/locales.pdf
## Current status
The sessions `ASpec` and `AInvs` are split, but other proofs remain duplicated