It is clear now that nobody later was influenced or aware of either. The abstract was too vague. It was written also prior to the completed thesis.
The two citations are: MacLane, Saunders, (Nov 1933) Jan 1934, Abbreviated Proofs in Logic Calculus, Bulletin of the American Mathematical Society 40(1):37--38.
MacLane, Saunders, 1934, Abgekuerzte Beweise in Logikkalkul, Goettingen: Hubert.
The thesis had insignificant distribution, mostly to the author's few dozen local friends (who had not interest in the subject). Weyl and Bernays saw it as the advisors, of course but didn't consider it much mathematics.
It goes: an input and the repetitive processes operating on it, a program, if worked, is equivalent all intermediate results of program execution and the output. Let this be a proof; if so we have two identical proofs, one often much shorter than the other but equally simple. They have same mathematical symbolic content, the same information we would say if it were binary.
We record the symbolic repetitive inference procedures as the axiom symbolic inference functions, to be recursively applied as needed rather than recording any results of their use. This works there is proof that these functions give valid inferences and can recursively operated with, that they can compress symbols systems.
It is a compression scheme for standard logical symbolic proofs, similar to sets of shorter sequences and chunks having same information as the symbols sequences they chunked but requiring less storage, eliminating the storage problem (Miller 1956, Pribram 1970), and considering as equivalent bits strings and fewer bit programs that output these measurements sequences and so normalizing to common units the strings by the programs (Solomonoff 1960, Chaitin 1966).