changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 67399 | eab6ce8368fa |
66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|
1 theory Hotel_Example_Prolog |
1 theory Hotel_Example_Prolog |
2 imports |
2 imports |
3 Hotel_Example |
3 Hotel_Example |
4 "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
4 "HOL-Library.Predicate_Compile_Alternative_Defs" |
5 "~~/src/HOL/Library/Code_Prolog" |
5 "HOL-Library.Code_Prolog" |
6 begin |
6 begin |
7 |
7 |
8 declare Let_def[code_pred_inline] |
8 declare Let_def[code_pred_inline] |
9 (* |
9 (* |
10 thm hotel_def |
10 thm hotel_def |