src/HOL/plain.ML
changeset 31259 c1b981b71dba
parent 29304 5c71a6da989d
child 33615 261abc2e3155
equal deleted inserted replaced
31258:43a418a41317 31259:c1b981b71dba