src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38958 08eb0ffa2413
parent 38954 80ce658600b0
child 38963 b5d126d7be4b