2010-05-27 wenzelm [Thu, 27 May 2010 17:41:27 +0200] rev 37145
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
NEWS src/HOL/Import/proof_kernel.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML src/HOL/Tools/hologic.ML src/HOL/Tools/primrec.ML src/HOLCF/Tools/Domain/domain_library.ML src/HOLCF/Tools/Domain/domain_theorems.ML src/Pure/Isar/class_target.ML src/Pure/Isar/expression.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_insts.ML src/Pure/Isar/specification.ML src/Pure/Proof/proof_syntax.ML src/Pure/ROOT.ML src/Pure/Thy/thy_output.ML src/Pure/old_goals.ML src/Pure/sign.ML src/Pure/type_infer.ML src/Pure/variable.ML src/Tools/nbe.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/inductive_package.ML src/ZF/ind_syntax.ML

2010-05-27 wenzelm [Thu, 27 May 2010 15:28:23 +0200] rev 37144
misc updates for release;
CONTRIBUTORS NEWS

2010-05-27 wenzelm [Thu, 27 May 2010 15:15:20 +0200] rev 37143
constant Rat.normalize needs to be qualified;
NEWS src/HOL/Rat.thy

2010-05-27 wenzelm [Thu, 27 May 2010 13:13:30 +0200] rev 37142
merged

2010-05-27 haftmann [Thu, 27 May 2010 08:02:02 +0200] rev 37141
merged

2010-05-26 haftmann [Wed, 26 May 2010 16:44:57 +0200] rev 37140
dropped legacy theorem bindings
src/HOLCF/IOA/Modelcheck/MuIOA.thy src/HOLCF/IOA/meta_theory/Sequence.thy

2010-05-26 haftmann [Wed, 26 May 2010 16:31:44 +0200] rev 37139
dropped legacy theorem bindings
src/HOL/MicroJava/J/Conform.thy src/HOL/Modelcheck/MuckeSyn.thy

2010-05-26 haftmann [Wed, 26 May 2010 16:28:55 +0200] rev 37138
dropped legacy theorem bindings
src/HOL/Bali/AxExample.thy src/HOL/Hoare/hoare_tac.ML

2010-05-26 haftmann [Wed, 26 May 2010 16:17:30 +0200] rev 37137
dropped legacy theorem bindings
src/HOL/Nominal/nominal_induct.ML

2010-05-26 haftmann [Wed, 26 May 2010 16:05:25 +0200] rev 37136
dropped legacy theorem bindings
src/HOL/Hoare_Parallel/OG_Tactics.thy src/HOL/Product_Type.thy src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/quickcheck_generators.ML src/HOL/Tools/record.ML