src/HOL/HOL.ML
changeset 20145 922b4e7b8efd
parent 18916 fda5b8dbbef6
child 20944 34b2c1bb7178
equal deleted inserted replaced
20144:2517cd4b1f37 20145:922b4e7b8efd