adbrucker/isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Added note that Hiding_Type_Variables.thy is also included in the AFP.

Browse Source
This commit is contained in:
Achim D. Brucker 2023-07-15 17:46:23 +01:00
parent 840c2d63ed
commit a73e2e5245
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
README.md
View File

@ -27,7 +27,11 @@ older versions might be available on a dedicated branch.
e.g., `('a, 'b, 'c) foo` is shown as `(_) foo`. This shorthand
notation can also be used in input (using a parse translation),
which (sometimes) helps to focus on the important parts of complex
type declarations.
type declarations. This setup is used by the AFP entries
[ A Formal Model of the Document Object Model](https://www.isa-afp.org/entries/Core_DOM.html)
and [ The Safely Composable DOM](https://www.isa-afp.org/entries/Core_SC_DOM.html):
a copy of this theory is included in these AFP entries and, hence, it can be
used by importing either of these AFP entries.
* [Ml_Yacc_Lib.thy](Ml_Yacc_Lib.thy) provides Isabelle support for parser
generated by ml-yacc (part of sml/NJ).