src/HOL/Real/PRat.thy
changeset 5548 5cd3396802f5
parent 5078 7b5ea59c0275
child 7077 60b098bb8b8a
equal deleted inserted replaced
5547:29f09a778037 5548:5cd3396802f5