src/Pure/General/basics.ML
changeset 58174 e51b4c7685a9
parent 51930 52fd62618631
child 61845 c5c7bc41185c
equal deleted inserted replaced
58173:7a259137a0ba 58174:e51b4c7685a9