src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 55370 e6be866b5f5b
parent 54489 03ff4d1e6784
child 55414 eab03e9cee8a