src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 40940 ff805bb109d8
parent 40924 a9be7f26b4e6
child 41231 2e901158675e