src/Pure/context.ML
changeset 22473 753123c89d72
parent 22149 7a8c2a556d28
child 22599 d920d38f1f02
equal deleted inserted replaced
22472:bfd9c0fd70b1 22473:753123c89d72