src/HOL/Library/SCT_Definition.thy
changeset 23767 7272a839ccd9
parent 23416 b73a6b72f706