equal
deleted
inserted
replaced
202 primitive Thm.assume_hyps. |
202 primitive Thm.assume_hyps. |
203 |
203 |
204 * Inner syntax token language allows regular quoted strings "..." |
204 * Inner syntax token language allows regular quoted strings "..." |
205 (only makes sense in practice, if outer syntax is delimited |
205 (only makes sense in practice, if outer syntax is delimited |
206 differently). |
206 differently). |
|
207 |
|
208 * Command 'print_term_bindings' supersedes 'print_binds' for clarity, |
|
209 but the latter is retained some time as Proof General legacy. |
207 |
210 |
208 |
211 |
209 *** HOL *** |
212 *** HOL *** |
210 |
213 |
211 * Command and antiquotation ''value'' are hardcoded against nbe and |
214 * Command and antiquotation ''value'' are hardcoded against nbe and |