src/HOL/HOL.ML
changeset 5253 82a5ca6290aa
parent 5228 66925577cefe
child 5299 d15a4155b96b