src/HOL/Library/SCT_Theorem.thy
changeset 22567 1565d476a9e2
parent 22371 c9f5895972b0
child 22665 cf152ff55d16