src/HOL/Import/HOL4Compat.thy
changeset 37724 6607ccf77946
parent 37596 248db70c9bcf
child 39246 9e58f0499f57