src/Pure/context.ML
changeset 36615 88756a5a92fc
parent 36610 bafd82950e24
child 37216 3165bc303f66
equal deleted inserted replaced
36614:b6c031ad3690 36615:88756a5a92fc