src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 40459 913e545d9a9b
parent 40054 cd7b1fa20bce
child 40548 54eb5fd36e5e
equal deleted inserted replaced
40458:12c8c64203b3 40459:913e545d9a9b