src/Pure/pure_syn.ML
changeset 66452 450cefec7c11
parent 64556 851ae0e7b09c
child 67381 146757999c8d
equal deleted inserted replaced
66450:a8299195ed82 66452:450cefec7c11