Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. missing latex font
  2. Rewrite: added links to docu, made more prominent
Changeset 74889:7dbac7d3cdab by nipkow:
missing latex font
The file was modified src/HOL/Examples/Rewrite_Examples.thy (diff)
The file was modified src/HOL/Examples/document/root.tex (diff)
Changeset 74888:1c50ddcf6a01 by nipkow:
Rewrite: added links to docu, made more prominent
The file was addedsrc/HOL/Examples/Rewrite_Examples.thy
The file was modified src/HOL/Library/Rewrite.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/ex/Rewrite_Examples.thy