2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:48 +0200] rev 24590
delayed evaluation
src/Tools/nbe.ML

2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:44 +0200] rev 24589
clarified class interfaces and internals
src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_package.ML src/Pure/Isar/class.ML src/Pure/Isar/isar_syn.ML src/Pure/axclass.ML

2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:43 +0200] rev 24588
introduced classes
src/HOL/Real/RealVector.thy

2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:42 +0200] rev 24587
multi-functional value keyword
src/HOL/Library/Eval.thy src/HOL/ex/Eval_Examples.thy

2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:41 +0200] rev 24586
added lemmas for finiteness
src/HOL/Finite_Set.thy

2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:40 +0200] rev 24585
tuned
doc-src/TutorialI/Misc/appendix.thy src/HOL/ex/Fundefs.thy src/Pure/Isar/code.ML src/Pure/codegen.ML src/Tools/code/code_package.ML

2007-09-15 haftmann [Sat, 15 Sep 2007 19:27:35 +0200] rev 24584
fixed title
Admin/de_overload.ML doc-src/AxClass/Nat/NatClass.ML doc-src/antiquote_setup.ML src/FOLP/FOLP_lemmas.ML src/FOLP/ex/Nat.ML src/FOLP/ex/Prolog.ML src/FOLP/intprover.ML src/HOL/Hoare/ROOT.ML src/HOL/Import/xml.ML src/HOL/Matrix/cplex/matrixlp.ML src/HOL/Nominal/ROOT.ML src/HOL/Real/float_arith.ML src/HOL/TLA/ROOT.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Qelim/cooper_data.ML src/HOL/Tools/Qelim/ferrante_rackoff.ML src/HOL/Tools/Qelim/ferrante_rackoff_data.ML src/HOL/Tools/Qelim/generated_cooper.ML src/HOL/Tools/Qelim/presburger.ML src/HOL/Tools/function_package/fundef_lib.ML src/HOL/Tools/function_package/pattern_split.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/split_rule.ML src/HOL/Tools/watcher.ML src/HOL/ex/svc_funcs.ML src/HOLCF/IOA/ABP/ROOT.ML src/HOLCF/IOA/NTP/ROOT.ML src/HOLCF/IOA/ROOT.ML src/HOLCF/IOA/Storage/ROOT.ML src/HOLCF/IOA/ex/ROOT.ML src/Provers/Arith/abel_cancel.ML src/Pure/General/xml.ML src/Pure/ML-Systems/overloading_smlnj.ML src/Pure/ML-Systems/polyml-5.1.ML src/Pure/ProofGeneral/pgml.ML src/Pure/Thy/html.ML src/Sequents/LK/ROOT.ML src/Sequents/modal.ML src/Tools/Compute_Oracle/am_compiler.ML src/Tools/Compute_Oracle/am_ghc.ML src/Tools/Compute_Oracle/am_interpreter.ML src/Tools/Compute_Oracle/am_sml.ML src/Tools/Compute_Oracle/compute.ML src/Tools/Compute_Oracle/linker.ML src/Tools/float.ML src/Tools/integer.ML src/Tools/rat.ML src/ZF/Coind/ROOT.ML src/ZF/Tools/cartprod.ML ...

2007-09-15 wenzelm [Sat, 15 Sep 2007 19:26:28 +0200] rev 24583
replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
src/Pure/Syntax/lexicon.ML

2007-09-15 wenzelm [Sat, 15 Sep 2007 19:26:17 +0200] rev 24582
ML_Lex.keywords;
tuned comments;
src/Pure/ML/ml_syntax.ML

2007-09-15 wenzelm [Sat, 15 Sep 2007 19:26:06 +0200] rev 24581
tuned comments;
src/Pure/ML/ml_context.ML