src/HOL/Induct/QuoDataType.thy
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 75287 7add2d5322a7
equal deleted inserted replaced
69980:f2e3adfd916f 69981:3dced198b9ec