src/HOL/HOL.ML
changeset 8857 7ec405405dd7
parent 7529 fa534e4f7e49
child 9396 a1b31d61f8e1
equal deleted inserted replaced
8856:435187ffc64e 8857:7ec405405dd7