src/Pure/General/basics.ML
changeset 48913 f686cb016c0c
parent 41493 f05976d69141
child 51930 52fd62618631
equal deleted inserted replaced
48912:ffdb37019b2f 48913:f686cb016c0c