src/HOL/Library/SCT_Theorem.thy
changeset 23521 195fe3fe2831
parent 23416 b73a6b72f706