| #
f7be4216 |
|
16-Aug-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Remove _TY_DEF theorems from most OpenTheory packages in src
These theorems are never used, and usually have ugly large terms, so it
seems better to strip them out of packages.
|
| #
bd584852 |
|
07-Jun-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Rename hol4-string-unint.art, and bump version number
The version needs to change before upload because the author changed.
|
| #
6b87368a |
|
20-May-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Change author on OpenTheory packages
from HOL developers to HOL OpenTheory Packager
|
| #
d818c14c |
|
26-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Split out and re-use HOL interpretation
OpenTheory now supports importing an interpretation from a file.
|
| #
b01d0154 |
|
05-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Add some show directives to hol4-string.thy
|
| #
1195276c |
|
02-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Add a hol-string package
Contains all the theories in src/string. Unfortunately this method
requires the HOL4 interpretation to be copied...
|