src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 46788 aefdc0095d7e
parent 45970 b6d0cff57d96
child 46884 154dc6ec0041
equal deleted inserted replaced
46787:3d3d8f8929a7 46788:aefdc0095d7e