src/Pure/ROOT0.ML
changeset 73068 a95f5ae5a12a
parent 72031 b7cec26e41d1
child 80801 090adcdceaae
equal deleted inserted replaced
73067:d045d900a929 73068:a95f5ae5a12a