src/HOL/Tools/recdef.ML
changeset 67161 b762ed417ed9
parent 60520 09fc5eaa21ce
equal deleted inserted replaced
67160:f37bf261bdf6 67161:b762ed417ed9