aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Base.thy
diff options
context:
space:
mode:
authorJosh Chen2019-02-11 10:46:16 +0100
committerJosh Chen2019-02-11 10:46:16 +0100
commitda8edcc1162044c33053ea64c4efbd4910b6cec7 (patch)
tree0321452c742939ed13da1938a6aaa259374253af /HoTT_Base.thy
parent91dc4798571fa99d68ced7ba098c958fca94c477 (diff)
get_this more robust. Functions to convert ML terms and types to strings.
Diffstat (limited to 'HoTT_Base.thy')
0 files changed, 0 insertions, 0 deletions