2010-06-11 blanchet [Fri, 11 Jun 2010 16:34:56 +0200] rev 37396
remove needless variables
src/HOL/Tools/Nitpick/minipick.ML src/HOL/Tools/Nitpick/nitpick_tests.ML

2010-06-11 haftmann [Fri, 11 Jun 2010 16:52:17 +0200] rev 37395
hide sum explicitly
src/HOL/ex/Meson_Test.thy

2010-06-10 haftmann [Thu, 10 Jun 2010 12:28:27 +0200] rev 37394
merged

2010-06-10 haftmann [Thu, 10 Jun 2010 12:26:07 +0200] rev 37393
adjust popular symbolic type constructors
src/Pure/Isar/class_target.ML

2010-06-10 haftmann [Thu, 10 Jun 2010 12:25:14 +0200] rev 37392
tailored set of code equations manually
src/HOL/ex/Codegenerator_Candidates.thy

2010-06-10 haftmann [Thu, 10 Jun 2010 12:24:03 +0200] rev 37391
tuned quotes, antiquotations and whitespace
src/HOL/Decision_Procs/Approximation.thy src/HOL/Hoare/hoare_tac.ML src/HOL/Import/Generate-HOL/GenHOL4Base.thy src/HOL/Import/Generate-HOLLight/GenHOLLight.thy src/HOL/Import/HOL/pair.imp src/HOL/Import/HOLLight/hollight.imp src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_permeq.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Tools/Function/function_lib.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/TFL/dcterm.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/usyntax.ML src/HOL/Tools/float_arith.ML src/HOL/Tools/refute.ML src/HOL/Transitive_Closure.thy src/HOLCF/IOA/Modelcheck/MuIOA.thy src/HOLCF/IOA/meta_theory/automaton.ML src/HOLCF/Tools/Domain/domain_library.ML src/HOLCF/Tools/Domain/domain_theorems.ML

2010-06-10 haftmann [Thu, 10 Jun 2010 12:24:02 +0200] rev 37390
moved inductive_codegen to place where product type is available; tuned structure name
src/HOL/Inductive.thy src/HOL/Library/SML_Quickcheck.thy src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_set.ML

2010-06-10 haftmann [Thu, 10 Jun 2010 12:24:01 +0200] rev 37389
qualified type "*"; qualified constants Pair, fst, snd, split
NEWS src/HOL/Product_Type.thy src/HOL/Tools/hologic.ML

2010-06-08 haftmann [Tue, 08 Jun 2010 16:37:22 +0200] rev 37388
tuned quotes, antiquotations and whitespace
src/HOL/Library/Binomial.thy src/HOL/Library/Countable.thy src/HOL/Library/Diagonalize.thy src/HOL/Library/Efficient_Nat.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Nominal/Examples/Support.thy src/HOL/SetInterval.thy src/HOL/Sum_Type.thy src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/groebner.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/meson.ML src/HOL/Tools/nat_numeral_simprocs.ML src/HOL/Tools/refute.ML src/HOL/ex/Dedekind_Real.thy src/HOL/ex/Refute_Examples.thy

2010-06-08 haftmann [Tue, 08 Jun 2010 16:37:19 +0200] rev 37387
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
NEWS src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Import/HOL/num.imp src/HOL/Import/HOL/pair.imp src/HOL/Import/HOLLight/hollight.imp src/HOL/Nat.thy src/HOL/Product_Type.thy src/HOL/Set.thy src/HOL/Tools/Function/measure_functions.ML src/HOL/Tools/Function/sum_tree.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/hologic.ML