src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 40177 30482e17955b
parent 40137 9eabcb1bfe50
child 40658 5ccfc3ee7fe6