summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 21 Nov 2006 20:47:58 +0100 | |

changeset 21447 | 379f130843f7 |

parent 21446 | 3d57db34633b |

child 21448 | 09c953c07008 |

* Isar: the assumptions of a long theorem statement are available as assms;

NEWS | file | annotate | diff | comparison | revisions | |

doc-src/IsarRef/pure.tex | file | annotate | diff | comparison | revisions |

--- a/NEWS Tue Nov 21 18:50:54 2006 +0100 +++ b/NEWS Tue Nov 21 20:47:58 2006 +0100 @@ -218,6 +218,11 @@ resulting rule, for later use with the 'cases' method (cf. attribute case_names). +* Isar: the assumptions of a long theorem statement are available as +"assms" fact in the proof context. This is more appropriate than the +(historical) "prems", which refers to all assumptions of the current +context, including those from the target locale, proof body etc. + * Isar: 'print_statement' prints theorems from the current theory or proof context in long statement form, according to the syntax of a top-level lemma.

--- a/doc-src/IsarRef/pure.tex Tue Nov 21 18:50:54 2006 +0100 +++ b/doc-src/IsarRef/pure.tex Tue Nov 21 20:47:58 2006 +0100 @@ -892,13 +892,14 @@ Claims at the theory level may be either in short or long form. A short goal merely consists of several simultaneous propositions (often just one). A long goal includes an explicit context specification for -the subsequent conclusion, involving local parameters. Here the role -of each part of the statement is explicitly marked by separate -keywords (see also \S\ref{sec:locale}). -\indexisarelem{shows}\indexisarelem{obtains}Moreover, there are two -kinds of conclusions: $\isarkeyword{shows}$ states several -simultaneous propositions (essentially a big conjunction), while -$\isarkeyword{obtains}$ claims several simultaneous simultaneous +the subsequent conclusion, involving local parameters and assumptions. +Here the role of each part of the statement is explicitly marked by +separate keywords (see also \S\ref{sec:locale}); the local assumptions +being introduced here are available as $assms$\indexisarthm{assms} in +the proof. \indexisarelem{shows}\indexisarelem{obtains}Moreover, +there are two kinds of conclusions: $\isarkeyword{shows}$ states +several simultaneous propositions (essentially a big conjunction), +while $\isarkeyword{obtains}$ claims several simultaneous simultaneous contexts of (essentially a big disjunction of eliminated parameters and assumptions, cf.\ \S\ref{sec:obtain}).