src/HOL/indrule.ML
changeset 1444 23ceb1dc9755
parent 1424 ccb3c5ff6707
child 1465 5d7a7e439cec