src/HOL/BCV/Orders0.ML
changeset 7999 7acf6eb8eec1
parent 7961 422ac6888c7f
child 8423 3c19160b6432
equal deleted inserted replaced
7998:3d0c34795831 7999:7acf6eb8eec1