src/Pure/General/binding.ML
changeset 64224 3ed43cfc8b14
parent 63369 4698dd1106ae
child 70494 41108e3e9ca5
equal deleted inserted replaced
64223:9d5b9f41df77 64224:3ed43cfc8b14