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

author | nipkow |

Thu, 19 May 2005 18:07:05 +0200 | |

changeset 16010 | 0705c8d1f107 |

parent 16009 | a6d480e6c5f0 |

child 16011 | 237aafbdb1f4 |

subst again

--- a/doc-src/IsarRef/generic.tex Thu May 19 11:08:15 2005 +0200 +++ b/doc-src/IsarRef/generic.tex Thu May 19 18:07:05 2005 +0200 @@ -903,7 +903,8 @@ $subst$ is not specified. \item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the -assumptions, which are treated as one big term. +assumptions. Positions $1 \dots i@1$ refer +to assumption 1, positions $i@1+1 \dots i@2$ to assumption 2, and so on. \item [$hypsubst$] performs substitution using some assumption; this only works for equations of the form $x = t$ where $x$ is a free or bound