src/HOL/intr_elim.ML
changeset 1444 23ceb1dc9755
parent 1425 7b61bcfeaa95
child 1465 5d7a7e439cec