basic setup for equational reasoning;
updated rewrite_goals_tac and fold_goals_tac;

--- a/doc-src/IsarImplementation/IsaMakefile	Tue Feb 07 18:56:40 2012 +0100
+++ b/doc-src/IsarImplementation/IsaMakefile	Thu Feb 09 19:34:23 2012 +0100
@@ -21,10 +21,10 @@
 
 Thy: $(LOG)/HOL-Thy.gz
 
-$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy		\
-  Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy	\
-  Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy		\
-  ../antiquote_setup.ML
+$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Eq.thy			\
+  Thy/Integration.thy Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy	\
+  Thy/Prelim.thy Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy		\
+  Thy/ML.thy ../antiquote_setup.ML
 	@$(USEDIR) HOL Thy
 	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
 	 Thy/document/pdfsetup.sty Thy/document/session.tex

--- a/doc-src/IsarImplementation/Makefile	Tue Feb 07 18:56:40 2012 +0100
+++ b/doc-src/IsarImplementation/Makefile	Thu Feb 09 19:34:23 2012 +0100
@@ -13,11 +13,12 @@
 FILES = ../extra.sty ../iman.sty ../../lib/texinputs/isabelle.sty	\
   ../../lib/texinputs/isabellesym.sty					\
   ../../lib/texinputs/railsetup.sty ../isar.sty ../manual.bib		\
-  ../pdfsetup.sty ../proof.sty Thy/document/Integration.tex		\
-  Thy/document/Isar.tex Thy/document/Local_Theory.tex			\
-  Thy/document/Logic.tex Thy/document/Prelim.tex			\
-  Thy/document/Proof.tex Thy/document/Syntax.tex			\
-  Thy/document/Tactic.tex implementation.tex style.sty
+  ../pdfsetup.sty ../proof.sty Thy/document/Eq.tex			\
+  Thy/document/Integration.tex Thy/document/Isar.tex			\
+  Thy/document/Local_Theory.tex Thy/document/Logic.tex			\
+  Thy/document/Prelim.tex Thy/document/Proof.tex			\
+  Thy/document/Syntax.tex Thy/document/Tactic.tex implementation.tex	\
+  style.sty
 
 dvi: $(NAME).dvi
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/Eq.thy	Thu Feb 09 19:34:23 2012 +0100
@@ -0,0 +1,75 @@
+theory Eq
+imports Base
+begin
+
+chapter {* Equational reasoning *}
+
+text {* Equality is one of the most fundamental concepts of
+  mathematics.  The Isabelle/Pure logic (\chref{ch:logic}) provides a
+  builtin relation @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} that expresses equality
+  of arbitrary terms (or propositions) at the framework level, as
+  expressed by certain basic inference rules (\secref{sec:eq-rules}).
+
+  Equational reasoning means to replace equals by equals, using
+  reflexivity and transitivity to form chains of replacement steps,
+  and congruence rules to access sub-structures.  Conversions
+  (\secref{sec:conv}) provide a convenient framework to compose basic
+  equational steps to build specific equational reasoning tools.
+
+  Higher-order matching is able to provide suitable instantiations for
+  giving equality rules, which leads to the versatile concept of
+  @{text "\<lambda>"}-term rewriting (\secref{sec:rewriting}).  Internally
+  this is based on the general-purpose Simplifier engine of Isabelle,
+  which is more specific and more efficient than plain conversions.
+
+  Object-logics usually introduce specific notions of equality or
+  equivalence, and relate it with the Pure equality.  This enables to
+  re-use the Pure tools for equational reasoning for particular
+  object-logic connectives as well.
+*}
+
+
+section {* Basic equality rules \label{sec:eq-rules} *}
+
+text {* FIXME *}
+
+
+section {* Conversions \label{sec:conv} *}
+
+text {* FIXME *}
+
+
+section {* Rewriting \label{sec:rewriting} *}
+
+text {* Rewriting normalizes a given term (theorem or goal) by
+  replacing instances of given equalities @{text "t \<equiv> u"} in subterms.
+  Rewriting continues until no rewrites are applicable to any subterm.
+  This may be used to unfold simple definitions of the form @{text "f
+  x\<^sub>1 \<dots> x\<^sub>n \<equiv> u"}, but is slightly more general than that.
+*}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML rewrite_goal_tac: "thm list -> int -> tactic"} \\
+  @{index_ML rewrite_goals_tac: "thm list -> tactic"} \\
+  @{index_ML fold_goals_tac: "thm list -> tactic"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML rewrite_goal_tac}~@{text "rules i"} rewrites subgoal
+  @{text "i"} by the given rewrite rules.
+
+  \item @{ML rewrite_goals_tac}~@{text "rules"} rewrites all subgoals
+  by the given rewrite rules.
+
+  \item @{ML fold_goals_tac}~@{text "rules"} essentially uses @{ML
+  rewrite_goals_tac} with the symmetric form of each member of @{text
+  "rules"}, re-ordered to fold longer expression first.  This supports
+  to idea to fold primitive definitions that appear in expended form
+  in the proof state.
+
+  \end{description}
+*}
+
+end

--- a/doc-src/IsarImplementation/Thy/ROOT.ML	Tue Feb 07 18:56:40 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Thu Feb 09 19:34:23 2012 +0100
@@ -1,4 +1,5 @@
 use_thys [
+  "Eq",
   "Integration",
   "Isar",
   "Local_Theory",

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/Eq.tex	Thu Feb 09 19:34:23 2012 +0100
@@ -0,0 +1,135 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Eq}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Eq\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Equational reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Equality is one of the most fundamental concepts of
+  mathematics.  The Isabelle/Pure logic (\chref{ch:logic}) provides a
+  builtin relation \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} that expresses equality
+  of arbitrary terms (or propositions) at the framework level, as
+  expressed by certain basic inference rules (\secref{sec:eq-rules}).
+
+  Equational reasoning means to replace equals by equals, using
+  reflexivity and transitivity to form chains of replacement steps,
+  and congruence rules to access sub-structures.  Conversions
+  (\secref{sec:conv}) provide a convenient framework to compose basic
+  equational steps to build specific equational reasoning tools.
+
+  Higher-order matching is able to provide suitable instantiations for
+  giving equality rules, which leads to the versatile concept of
+  \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-term rewriting (\secref{sec:rewriting}).  Internally
+  this is based on the general-purpose Simplifier engine of Isabelle,
+  which is more specific and more efficient than plain conversions.
+
+  Object-logics usually introduce specific notions of equality or
+  equivalence, and relate it with the Pure equality.  This enables to
+  re-use the Pure tools for equational reasoning for particular
+  object-logic connectives as well.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Basic equality rules \label{sec:eq-rules}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conversions \label{sec:conv}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Rewriting \label{sec:rewriting}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Rewriting normalizes a given term (theorem or goal) by
+  replacing instances of given equalities \isa{t\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u} in subterms.
+  Rewriting continues until no rewrites are applicable to any subterm.
+  This may be used to unfold simple definitions of the form \isa{f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u}, but is slightly more general than that.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{rewrite\_goal\_tac}\verb|rewrite_goal_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{rewrite\_goals\_tac}\verb|rewrite_goals_tac: thm list -> tactic| \\
+  \indexdef{}{ML}{fold\_goals\_tac}\verb|fold_goals_tac: thm list -> tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|rewrite_goal_tac|~\isa{rules\ i} rewrites subgoal
+  \isa{i} by the given rewrite rules.
+
+  \item \verb|rewrite_goals_tac|~\isa{rules} rewrites all subgoals
+  by the given rewrite rules.
+
+  \item \verb|fold_goals_tac|~\isa{rules} essentially uses \verb|rewrite_goals_tac| with the symmetric form of each member of \isa{rules}, re-ordered to fold longer expression first.  This supports
+  to idea to fold primitive definitions that appear in expended form
+  in the proof state.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:

--- a/doc-src/IsarImplementation/implementation.tex	Tue Feb 07 18:56:40 2012 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Thu Feb 09 19:34:23 2012 +0100
@@ -86,6 +86,7 @@
 \input{Thy/document/Logic.tex}
 \input{Thy/document/Syntax.tex}
 \input{Thy/document/Tactic.tex}
+\input{Thy/document/Eq.tex}
 \input{Thy/document/Proof.tex}
 \input{Thy/document/Isar.tex}
 \input{Thy/document/Local_Theory.tex}

--- a/doc-src/Ref/tactic.tex	Tue Feb 07 18:56:40 2012 +0100
+++ b/doc-src/Ref/tactic.tex	Thu Feb 09 19:34:23 2012 +0100
@@ -29,44 +29,6 @@
 \end{ttdescription}
 
 
-\subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals}
-\index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
-\index{definitions}
-
-Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
-constant or a constant applied to a list of variables, for example $\it
-sqr(n)\equiv n\times n$.  Conditional definitions, $\phi\Imp t\equiv u$,
-are also supported.  {\bf Unfolding} the definition ${t\equiv u}$ means using
-it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
-Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
-no rewrites are applicable to any subterm.
-
-There are rules for unfolding and folding definitions; Isabelle does not do
-this automatically.  The corresponding tactics rewrite the proof state,
-yielding a single next state.
-\begin{ttbox} 
-rewrite_goals_tac : thm list -> tactic
-fold_goals_tac    : thm list -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{rewrite_goals_tac} {\it defs}]  
-unfolds the {\it defs} throughout the subgoals of the proof state, while
-leaving the main goal unchanged.  Use \ttindex{SELECT_GOAL} to restrict it to a
-particular subgoal.
-
-\item[\ttindexbold{fold_goals_tac} {\it defs}]  
-folds the {\it defs} throughout the subgoals of the proof state, while
-leaving the main goal unchanged.
-\end{ttdescription}
-
-\begin{warn}
-  These tactics only cope with definitions expressed as meta-level
-  equalities ($\equiv$).  More general equivalences are handled by the
-  simplifier, provided that it is set up appropriately for your logic
-  (see Chapter~\ref{chap:simplification}).
-\end{warn}
-
-
 \subsection{Composition: resolution without lifting}
 \index{tactics!for composition}
 \begin{ttbox}