src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 54611 31afce809794
parent 54489 03ff4d1e6784
child 55414 eab03e9cee8a
equal deleted inserted replaced
54610:6593e06445e6 54611:31afce809794