src/HOL/Tools/recdef.ML
changeset 71035 6fe5a0e1fa8e
parent 60520 09fc5eaa21ce
equal deleted inserted replaced
71034:e0755162093f 71035:6fe5a0e1fa8e