aboutsummaryrefslogtreecommitdiff
path: root/util.ML (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Remove all type inference functionality (feature development moving to ↵Josh Chen2019-02-281-124/+0
| | | | | | another branch). 2. Eq.thy complete.
* Put typing functionality into a .thy and clean up antiquotations, which ↵Josh Chen2019-02-111-35/+37
| | | | results in some reorganization of the theory import structure.
* get_this more robust. Functions to convert ML terms and types to strings.Josh Chen2019-02-111-3/+23
|
* restructure libraryJosh Chen2019-02-101-0/+102