src/Pure/library.ML
changeset 5978 fa2c2dd74f8c
parent 5966 60f80b2a2777
child 6282 589671bebbb3
equal deleted inserted replaced
5977:9f0c8869cf71 5978:fa2c2dd74f8c