src/Pure/pure_syn.ML
changeset 62890 728aa05e9433
parent 62876 507c90523113
child 62912 745d31e63c21