src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 39188 cd6558ed65d7
parent 38963 b5d126d7be4b
child 39189 d183bf90dabd
child 39198 f967a16dfcdd