src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
changeset 42207 2bda5eddadf3
parent 42142 d24a93025feb
child 42291 682b35dc1926