src/HOL/Tools/recdef_package.ML
changeset 31213 800787c3210f
parent 31172 74d72ba262fb
child 31243 4c34331a88f9
equal deleted inserted replaced
31212:a94aea0cef76 31213:800787c3210f