src/HOL/ex/Recdefs.thy
changeset 6213 f5bdd6497e08
parent 5502 da4d0444ea85
child 6455 34c6c2944908
equal deleted inserted replaced
6212:974310f9ca7d 6213:f5bdd6497e08