src/HOL/HOL.ML
changeset 2935 998cb95fdd43
parent 2562 d571d6660240
child 3003 c5293a17afa6
equal deleted inserted replaced
2934:bd922fc9001b 2935:998cb95fdd43