2011-08-08 wenzelm [Mon, 08 Aug 2011 17:23:15 +0200] rev 44058
misc tuning -- eliminated old-fashioned rep_thm;
src/HOL/Library/positivstellensatz.ML src/HOL/Orderings.thy src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/SMT/z3_proof_reconstruction.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/sat_funcs.ML src/Provers/hypsubst.ML src/Pure/Isar/element.ML src/Pure/Isar/rule_insts.ML src/Pure/Proof/proofchecker.ML src/Pure/raw_simplifier.ML src/Pure/simplifier.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/induct_tacs.ML src/ZF/arith_data.ML

2011-08-08 wenzelm [Mon, 08 Aug 2011 16:38:59 +0200] rev 44057
modernized strcture Proof_Checker;
src/Pure/Proof/extraction.ML src/Pure/Proof/proofchecker.ML

2011-08-08 wenzelm [Mon, 08 Aug 2011 16:09:34 +0200] rev 44056
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
src/Tools/jEdit/src/text_area_painter.scala

2011-08-08 wenzelm [Mon, 08 Aug 2011 13:48:38 +0200] rev 44055
updated imports;
doc-src/IsarRef/Thy/HOL_Specific.thy doc-src/IsarRef/Thy/document/HOL_Specific.tex

2011-08-08 wenzelm [Mon, 08 Aug 2011 13:40:24 +0200] rev 44054
proper signature;
src/Pure/Concurrent/bash.ML src/Pure/Concurrent/bash_sequential.ML

2011-08-08 wenzelm [Mon, 08 Aug 2011 13:39:51 +0200] rev 44053
made SML/NJ happy;
src/Pure/Isar/attrib.ML

2011-08-08 wenzelm [Mon, 08 Aug 2011 13:29:54 +0200] rev 44052
slightly more uniform messages;
src/HOL/Tools/Function/function.ML src/HOL/Tools/Metis/metis_tactics.ML src/Pure/codegen.ML

2011-08-08 wenzelm [Mon, 08 Aug 2011 13:19:19 +0200] rev 44051
avoid pointless completion of illegal control commands;
src/Pure/Isar/outer_syntax.scala

2011-08-08 nipkow [Mon, 08 Aug 2011 08:56:58 +0200] rev 44050
removed old expand_fun_eq
doc-src/TutorialI/Sets/sets.tex

2011-08-08 nipkow [Mon, 08 Aug 2011 08:25:28 +0200] rev 44049
fixed index entry
doc-src/TutorialI/fp.tex