equal
deleted
inserted
replaced
173 \item @{term "{ [x::int] | x. x \<le> -2 }"} |
173 \item @{term "{ [x::int] | x. x \<le> -2 }"} |
174 \end{itemize} |
174 \end{itemize} |
175 |
175 |
176 Hint: The third term is already quite big, and the pretty printer |
176 Hint: The third term is already quite big, and the pretty printer |
177 may omit parts of it by default. If you want to see all of it, you |
177 may omit parts of it by default. If you want to see all of it, you |
178 can use the following ML-function to set the printing depth to a higher |
178 need to set the printing depth to a higher value by |
179 value: |
|
180 |
|
181 @{ML [display,gray] "default_print_depth 50"} |
|
182 \end{exercise} |
179 \end{exercise} |
183 |
180 *} |
|
181 |
|
182 declare [[ML_print_depth = 50]] |
|
183 |
|
184 text {* |
184 The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the |
185 The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the |
185 usually invisible @{text "Trueprop"}-coercions whenever necessary. |
186 usually invisible @{text "Trueprop"}-coercions whenever necessary. |
186 Consider for example the pairs |
187 Consider for example the pairs |
187 |
188 |
188 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" |
189 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" |