src/HOL/Import/HOL4Compat.thy
changeset 38665 e92223c886f8
parent 37596 248db70c9bcf
child 39246 9e58f0499f57