equal
deleted
inserted
replaced
311 |
311 |
312 \medskip |
312 \medskip |
313 FIXME theory data |
313 FIXME theory data |
314 *} |
314 *} |
315 |
315 |
|
316 text %mlref {* |
|
317 *} |
|
318 |
316 |
319 |
317 subsection {* Proof context \label{sec:context-proof} *} |
320 subsection {* Proof context \label{sec:context-proof} *} |
318 |
321 |
319 text {* |
322 text {* |
320 A proof context is an arbitrary container that is initialized from a |
323 A proof context is an arbitrary container that is initialized from a |
348 generic notion of introducing and discharging hypotheses. Arbritrary |
351 generic notion of introducing and discharging hypotheses. Arbritrary |
349 auxiliary context data may be adjoined.} |
352 auxiliary context data may be adjoined.} |
350 |
353 |
351 *} |
354 *} |
352 |
355 |
|
356 text %mlref {* FIXME *} |
|
357 |
353 |
358 |
354 subsection {* Generic contexts *} |
359 subsection {* Generic contexts *} |
355 |
360 |
|
361 text FIXME |
|
362 |
|
363 text %mlref {* FIXME *} |
|
364 |
356 end |
365 end |