src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 60806 622d45ca75ee
parent 60500 903bb1495239
child 61125 4c68426800de
equal deleted inserted replaced
60804:080a979a985b 60806:622d45ca75ee