src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38944 827c98e8ba8b
parent 38734 e5508a74b11f
child 38949 1afa9e89c885