src/HOL/Library/SCT_Theorem.thy
changeset 23314 6894137e854a
parent 23014 00d8bf2fce42
child 23315 df3a7e9ebadb