2001-08-09 oheimb [Thu, 09 Aug 2001 10:17:45 +0200] rev 11493
added pair_imageI (also as intro rule)
src/HOL/Product_Type.thy

2001-08-09 oheimb [Thu, 09 Aug 2001 10:16:23 +0200] rev 11492
renamed addaltern to addafter, addSaltern to addSafter
NEWS

2001-08-08 wenzelm [Wed, 08 Aug 2001 17:39:32 +0200] rev 11491
added constify_ast_tr;
src/Pure/Syntax/syn_trans.ML

2001-08-08 wenzelm [Wed, 08 Aug 2001 17:39:16 +0200] rev 11490
field_name_ast_tr superceded by constify_ast_tr in Pure;
src/HOL/Tools/record_package.ML

2001-08-08 wenzelm [Wed, 08 Aug 2001 17:38:53 +0200] rev 11489
_constify;
src/HOL/Record.thy

2001-08-08 wenzelm [Wed, 08 Aug 2001 17:38:29 +0200] rev 11488
constify numeral tokens in order to allow translations;
src/HOL/Numeral.thy src/HOL/Tools/numeral_syntax.ML

2001-08-08 wenzelm [Wed, 08 Aug 2001 17:37:47 +0200] rev 11487
* HOL: syntax translations now work properly with numerals and records
expressions;
NEWS

2001-08-08 oheimb [Wed, 08 Aug 2001 16:57:43 +0200] rev 11486
layout, subscripts
src/HOL/NanoJava/AxSem.thy src/HOL/NanoJava/Decl.thy src/HOL/NanoJava/Equivalence.thy src/HOL/NanoJava/OpSem.thy src/HOL/NanoJava/Term.thy

2001-08-08 wenzelm [Wed, 08 Aug 2001 15:16:38 +0200] rev 11485
[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";
lib/scripts/run-polyml

2001-08-08 wenzelm [Wed, 08 Aug 2001 14:57:22 +0200] rev 11484
polyml-4.1.1;
Admin/polyml/bin/polyml-version