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

author | wenzelm |

Sat, 08 Jul 2006 14:12:13 +0200 | |

changeset 20065 | 636f84cd3639 |

parent 20064 | 92aad017b847 |

child 20066 | b045b835cb3b |

tuned;

doc-src/IsarImplementation/Thy/document/tactic.tex | file | annotate | diff | comparison | revisions | |

doc-src/IsarImplementation/Thy/tactic.thy | file | annotate | diff | comparison | revisions |

--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 14:01:40 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 14:12:13 2006 +0200 @@ -213,10 +213,6 @@ the quantifier prefix into schematic variables, and generalizing implicit type-variables. - Any additional fixed variables or hypotheses not being mentioned in - the initial statement are left unchanged --- programmed proofs may - well occur in a larger context. - \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual subgoals before commencing the actual proof.

--- a/doc-src/IsarImplementation/Thy/tactic.thy Sat Jul 08 14:01:40 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/tactic.thy Sat Jul 08 14:12:13 2006 +0200 @@ -174,10 +174,6 @@ the quantifier prefix into schematic variables, and generalizing implicit type-variables. - Any additional fixed variables or hypotheses not being mentioned in - the initial statement are left unchanged --- programmed proofs may - well occur in a larger context. - \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but states several conclusions simultaneously. @{ML Tactic.conjunction_tac} may be used to split these into individual