src/HOL/Hoare/Arith2.ML
changeset 17907 c20e4bddcb11
parent 17278 f27456a2a975