src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 75008 43b3d5318d72
parent 69593 3dda49e08b9d
child 82691 b69e4da2604b
equal deleted inserted replaced
75007:2e16798b6f2b 75008:43b3d5318d72