src/Pure/ML-Systems/proper_int.ML
changeset 25456 6f79698f294d
parent 24604 d5c5d2e13fbf
child 28490 40c3f900c457
equal deleted inserted replaced
25455:ab519be677ba 25456:6f79698f294d