src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 45919 2cae3d86abe5
parent 43888 ee4be704c2a4
child 48891 c0eafbd55de3