src/ZF/OrderArith.thy
changeset 82480 489f4a79d215
parent 76217 8655344f1cf6