src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 82905 c7e51784a3d5
parent 82774 2865a6618cba