src/HOL/Hoare/List_Examples.ML
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d