2010-10-29 blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40262
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Metis/metis_tactics.ML

2010-10-29 blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40261
more work on new Skolemizer without Hilbert_Choice
src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Metis/metis_reconstruct.ML

2010-10-29 blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40260
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
src/HOL/Tools/Meson/meson_clausify.ML

2010-10-29 blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40259
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
src/HOL/Tools/Metis/metis_reconstruct.ML src/HOL/Tools/Metis/metis_tactics.ML src/HOL/Tools/Metis/metis_translate.ML

2010-10-29 blanchet [Fri, 29 Oct 2010 12:49:05 +0200] rev 40258
make handling of parameters more robust, by querying the goal
src/HOL/Tools/Metis/metis_reconstruct.ML

2010-10-29 haftmann [Fri, 29 Oct 2010 11:35:28 +0200] rev 40257
actually pass "verbose" argument
src/Tools/Code/code_runtime.ML

2010-10-29 wenzelm [Fri, 29 Oct 2010 16:16:10 +0200] rev 40256
eliminated obsolete \_ escape;
doc-src/IsarRef/Thy/Spec.thy doc-src/IsarRef/Thy/document/Spec.tex

2010-10-29 wenzelm [Fri, 29 Oct 2010 11:49:56 +0200] rev 40255
eliminated obsolete \_ escapes in rail environments;
doc-src/IsarImplementation/Thy/Logic.thy doc-src/IsarImplementation/Thy/document/Logic.tex doc-src/IsarRef/Thy/Document_Preparation.thy doc-src/IsarRef/Thy/Generic.thy doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/IsarRef/Thy/Inner_Syntax.thy doc-src/IsarRef/Thy/Misc.thy doc-src/IsarRef/Thy/Proof.thy doc-src/IsarRef/Thy/Spec.thy doc-src/IsarRef/Thy/ZF_Specific.thy doc-src/IsarRef/Thy/document/Document_Preparation.tex doc-src/IsarRef/Thy/document/Generic.tex doc-src/IsarRef/Thy/document/HOL_Specific.tex doc-src/IsarRef/Thy/document/Inner_Syntax.tex doc-src/IsarRef/Thy/document/Misc.tex doc-src/IsarRef/Thy/document/Proof.tex doc-src/IsarRef/Thy/document/Spec.tex doc-src/IsarRef/Thy/document/ZF_Specific.tex

2010-10-29 wenzelm [Fri, 29 Oct 2010 11:35:47 +0200] rev 40254
proper markup of formal text;
doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/IsarRef/Thy/document/HOL_Specific.tex

2010-10-29 wenzelm [Fri, 29 Oct 2010 11:07:21 +0200] rev 40253
merged
NEWS src/FOL/ex/Iff_Oracle.thy src/Tools/quickcheck.ML