src/HOL/Eisbach/Examples.thy
changeset 81275 5ed639c16ce7
parent 69597 ff784d5a5bfb