src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 62131 1baed43f453e
parent 61585 a9599d3d7610
child 62597 b3f2b8c906a6
equal deleted inserted replaced
62128:3201ddb00097 62131:1baed43f453e