src/HOL/HOL.ML
changeset 21318 edb595802d22
parent 21150 405ebd7ba881
child 21379 a0561695167a
equal deleted inserted replaced
21317:ebd2704ed33b 21318:edb595802d22