src/Pure/pure.ML
changeset 10403 2955ee2424ce
parent 8965 d46b36785c70
child 10931 ef2b1dd40db9