src/HOL/indrule.ML
changeset 3685 5b8c0c8f576e
parent 3402 9477a6410fe1
child 4807 013ba4c43832
equal deleted inserted replaced
3684:f677f0bc1cdf 3685:5b8c0c8f576e