src/HOL/Library/SCT_Theorem.thy
changeset 23024 70435ffe077d
parent 23014 00d8bf2fce42
child 23315 df3a7e9ebadb