2008-12-06 huffman [Sat, 06 Dec 2008 20:26:51 -0800] rev 29014
multiplication for type inat
src/HOL/Library/Nat_Infinity.thy

2008-12-06 huffman [Sat, 06 Dec 2008 20:25:31 -0800] rev 29013
fix proofs
src/HOL/Tools/ComputeNumeral.thy

2008-12-06 huffman [Sat, 06 Dec 2008 19:39:53 -0800] rev 29012
change lemmas to avoid using neg
src/HOL/Arith_Tools.thy src/HOL/Library/Nat_Infinity.thy src/HOL/NatBin.thy

2008-12-05 huffman [Fri, 05 Dec 2008 17:35:22 -0800] rev 29011
simplify less_nat_number_of
src/HOL/NatBin.thy

2008-12-05 huffman [Fri, 05 Dec 2008 17:26:16 -0800] rev 29010
add lemma le_nat_number_of
src/HOL/NatBin.thy

2008-12-06 wenzelm [Sat, 06 Dec 2008 12:18:05 +0100] rev 29009
merged

2008-12-06 haftmann [Sat, 06 Dec 2008 08:57:39 +0100] rev 29008
adapted to changes in binding module
doc-src/IsarImplementation/Thy/ML.thy doc-src/IsarImplementation/Thy/document/ML.tex doc-src/IsarImplementation/Thy/document/logic.tex doc-src/IsarImplementation/Thy/document/prelim.tex doc-src/IsarImplementation/Thy/logic.thy doc-src/IsarImplementation/Thy/prelim.thy

2008-12-06 haftmann [Sat, 06 Dec 2008 08:45:38 +0100] rev 29007
merged

2008-12-05 haftmann [Fri, 05 Dec 2008 18:43:42 +0100] rev 29006
Name.name_of -> Binding.base_name
src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/function_package/fundef_common.ML src/HOL/Tools/function_package/fundef_package.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/inductive_set_package.ML src/HOL/Tools/primrec_package.ML src/HOL/Tools/recdef_package.ML src/HOL/Tools/specification_package.ML src/HOLCF/Tools/fixrec_package.ML src/Pure/General/binding.ML src/Pure/Isar/class.ML src/Pure/Isar/constdefs.ML src/Pure/Isar/element.ML src/Pure/Isar/expression.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/local_defs.ML src/Pure/Isar/new_locale.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML src/Pure/Isar/theory_target.ML src/Pure/Tools/invoke.ML src/Pure/name.ML src/Pure/sign.ML src/ZF/Tools/inductive_package.ML src/ZF/Tools/primrec_package.ML

2008-12-05 haftmann [Fri, 05 Dec 2008 18:42:39 +0100] rev 29005
corrected theory path
src/HOL/ROOT.ML