src/Pure/term.ML
changeset 863 67692db44c70
parent 728 9a973c3ba350
child 949 83c588d6fee9