src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 56717 d96b10ec397c
parent 48891 c0eafbd55de3
child 62390 842917225d56
equal deleted inserted replaced
56716:6d5733303a50 56717:d96b10ec397c