src/Pure/ROOT.ML
changeset 82874 abfb6ed8ec21
parent 82805 61aae966dd95
child 82948 e2e43992f339
equal deleted inserted replaced
82873:e567fd948ff0 82874:abfb6ed8ec21