src/HOL/Tools/recdef_package.ML
changeset 18703 13e11abcfc96
parent 18688 abf0f018b5ec
child 18708 4b3dadb4fe33