src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 80175 200107cdd3ac
parent 67613 ce654b0e6d69
equal deleted inserted replaced
80174:32d2b96affc7 80175:200107cdd3ac