src/Pure/System/session.ML
changeset 48017 9f7b27635b57
parent 46970 9667e0dcb5e2
child 48418 1a634f9614fb
equal deleted inserted replaced
48016:edbc8e8accd9 48017:9f7b27635b57