src/HOL/HOL.ML
changeset 21083 a1de02f047d0
parent 21009 0eae3fb48936
child 21150 405ebd7ba881
equal deleted inserted replaced
21082:82460fa3340d 21083:a1de02f047d0