2010-05-27 wenzelm [Thu, 27 May 2010 18:10:37 +0200] rev 37146
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
NEWS src/FOL/ex/Locale_Test/Locale_Test1.thy src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Modelcheck/EindhovenSyn.thy src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML src/HOLCF/IOA/meta_theory/automaton.ML src/Pure/General/print_mode.ML src/Pure/Isar/class_target.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/theory_target.ML src/Pure/ProofGeneral/pgip_parser.ML src/Pure/ROOT.ML src/Pure/Syntax/syntax.ML src/Pure/Thy/html.ML src/Pure/Thy/thy_output.ML src/Pure/codegen.ML src/Pure/consts.ML src/Tools/Code/code_printer.ML src/Tools/WWW_Find/html_unicode.ML src/Tools/nbe.ML src/Tools/value.ML

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