summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Intro/foundations.tex

changeset 6592 | c120262044b6 |

parent 6170 | 9a59cf8ae9b5 |

child 9695 | ec7d7f877712 |

--- a/doc-src/Intro/foundations.tex Wed May 05 14:31:31 1999 +0200 +++ b/doc-src/Intro/foundations.tex Wed May 05 16:44:42 1999 +0200 @@ -959,7 +959,7 @@ rather than on individual subgoals. An Isabelle tactic is a function that takes a proof state and returns a sequence (lazy list) of possible successor states. Lazy lists are coded in ML as functions, a standard -technique~\cite{paulson91}. Isabelle represents proof states by theorems. +technique~\cite{paulson-ml2}. Isabelle represents proof states by theorems. Basic tactics execute the meta-rules described above, operating on a given subgoal. The {\bf resolution tactics} take a list of rules and