src/HOL/Library/ROOT.ML
changeset 45615 c05e8209a3aa
parent 45483 34d07cf7d207
child 45985 2d399a776de2
equal deleted inserted replaced
45614:e19788cb0a1a 45615:c05e8209a3aa