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