src/Pure/type.ML
changeset 8771 026f37a86ea7
parent 8721 453b493ece0a
child 8899 99266fe189a1
equal deleted inserted replaced
8770:bfab4d4b7516 8771:026f37a86ea7