src/HOL/indrule.ML
changeset 4950 226f2cde9f4d
parent 4807 013ba4c43832
child 4971 09b8945cac07