src/Pure/ML-Systems/proper_int.ML
changeset 44238 36120feb70ed
parent 43948 8f5add916a99
child 45030 9cf265a192f6
equal deleted inserted replaced
44237:2a2040c9d898 44238:36120feb70ed