--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 14 21:22:13 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Apr 14 21:22:48 2010 +0200
@@ -471,7 +471,7 @@
Note that the resulting simplification and induction rules
correspond to the transformed specification, not the one given
originally. This usually means that each equation given by the user
- may result in several theroems. Also note that this automatic
+ may result in several theorems. Also note that this automatic
transformation only works for ML-style datatype patterns.
\item @{text domintros} enables the automated generation of
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 14 21:22:13 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Apr 14 21:22:48 2010 +0200
@@ -479,7 +479,7 @@
Note that the resulting simplification and induction rules
correspond to the transformed specification, not the one given
originally. This usually means that each equation given by the user
- may result in several theroems. Also note that this automatic
+ may result in several theorems. Also note that this automatic
transformation only works for ML-style datatype patterns.
\item \isa{domintros} enables the automated generation of
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Apr 14 21:22:13 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Apr 14 21:22:48 2010 +0200
@@ -174,6 +174,14 @@
\begin{quote}
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
\end{quote}
+Variables that are bound by quantifiers or lambdas cannot be renamed
+like this. Instead, the attribute \texttt{rename\_abs} does the
+job. It expects a list of names or underscores, similar to the
+\texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\end{quote}
+produces @{thm split_paired_All[rename_abs _ l r]}.
*}
subsection "Inference rules"
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Wed Apr 14 21:22:13 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Wed Apr 14 21:22:48 2010 +0200
@@ -233,7 +233,15 @@
\isa{fst\ {\isacharparenleft}a{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ a} is produced by
\begin{quote}
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
-\end{quote}%
+\end{quote}
+Variables that are bound by quantifiers or lambdas cannot be renamed
+like this. Instead, the attribute \texttt{rename\_abs} does the
+job. It expects a list of names or underscores, similar to the
+\texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\end{quote}
+produces \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}l\ r{\isachardot}\ P\ {\isacharparenleft}l{\isacharcomma}\ r{\isacharparenright}{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/HOL/Tools/record.ML Wed Apr 14 21:22:13 2010 +0200
+++ b/src/HOL/Tools/record.ML Wed Apr 14 21:22:48 2010 +0200
@@ -901,7 +901,7 @@
val varifyT = varifyT midx;
fun mk_type_abbr subst name alphas =
- let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
+ let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in
Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
end;
@@ -912,7 +912,7 @@
SOME (name, _) =>
if name = last_ext then
let val subst = match schemeT T in
- if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
+ if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS))))
then mk_type_abbr subst abbr alphas
else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
--- a/src/Tools/jEdit/README_BUILD Wed Apr 14 21:22:13 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Wed Apr 14 21:22:48 2010 +0200
@@ -16,6 +16,8 @@
* jEdit 4.3.1 (final)
http://www.jedit.org/
+
+
Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
* jEdit plugins: