Summary
- avoid reference to invisible theorem, by using another one instead (suggested by Anders Schlichtkrull; the document's author is incomunicado)
- tuning
- typo (reported by Anders Schlichtkrull)
The file was modified | src/Doc/Locales/Examples3.thy (diff) |
The file was modified | src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff) |
The file was modified | src/Doc/Locales/Examples3.thy (diff) |