src/HOL/simpdata.ML
changeset 1637 b8a8ae2e5de1
parent 1548 afe750876848
child 1655 5be64540f275
equal deleted inserted replaced
1636:e18416e3e1d4 1637:b8a8ae2e5de1