src/HOL/Library/old_recdef.ML
changeset 61378 3e04c9ca001a
parent 61268 abe08fb15a12
child 61424 c3658c18b7bc
equal deleted inserted replaced
61377:517feb558c77 61378:3e04c9ca001a