2010-02-10 haftmann [Wed, 10 Feb 2010 15:14:01 +0100] rev 35095
minor metis proof tuning
src/HOL/Metis_Examples/Message.thy

2010-02-10 haftmann [Wed, 10 Feb 2010 14:12:40 +0100] rev 35094
merged
src/HOL/Library/Structure_Syntax.thy

2010-02-10 haftmann [Wed, 10 Feb 2010 14:12:30 +0100] rev 35093
NEWS
NEWS

2010-02-10 haftmann [Wed, 10 Feb 2010 14:12:04 +0100] rev 35092
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
src/HOL/Algebras.thy src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Groebner_Basis.thy src/HOL/Groups.thy src/HOL/Hoare/hoare_tac.ML src/HOL/Import/Generate-HOL/GenHOL4Base.thy src/HOL/Import/Generate-HOL/GenHOL4Real.thy src/HOL/Import/HOL/arithmetic.imp src/HOL/Import/HOL/prim_rec.imp src/HOL/Import/HOL/real.imp src/HOL/Import/HOL/realax.imp src/HOL/Mutabelle/Mutabelle.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Orderings.thy src/HOL/Rings.thy src/HOL/Tools/Function/lexicographic_order.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/inductive.ML src/HOL/Tools/int_arith.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/nat_arith.ML src/HOL/Tools/nat_numeral_simprocs.ML src/HOL/Tools/numeral_simprocs.ML src/HOL/Tools/refute.ML src/HOL/Tools/res_clause.ML src/HOL/ex/SVC_Oracle.thy src/HOL/ex/svc_funcs.ML

2010-02-10 haftmann [Wed, 10 Feb 2010 14:12:02 +0100] rev 35091
revert uninspired Structure_Syntax experiment
src/HOL/IsaMakefile src/HOL/Library/Library.thy src/HOL/Library/Structure_Syntax.thy

2010-02-10 haftmann [Wed, 10 Feb 2010 14:12:02 +0100] rev 35090
moved lemma field_le_epsilon from Real.thy to Fields.thy
src/HOL/Fields.thy src/HOL/Real.thy

2010-02-10 wenzelm [Wed, 10 Feb 2010 12:04:57 +0100] rev 35089
merged

2010-02-10 wenzelm [Wed, 10 Feb 2010 12:03:13 +0100] rev 35088
unset KODKODI explicitly -- apparently isatest patches settings cumulatively;
Admin/isatest/settings/at-mac-poly-5.1-para Admin/isatest/settings/at-poly-5.1-para-e Admin/isatest/settings/at-poly-dev-e Admin/isatest/settings/at-sml Admin/isatest/settings/at-sml-dev-e Admin/isatest/settings/at-sml-dev-p Admin/isatest/settings/at64-poly Admin/isatest/settings/at64-poly-5.1-para Admin/isatest/settings/at64-sml-dev Admin/isatest/settings/mac-poly64-M8 Admin/isatest/settings/mac-sml-dev Admin/isatest/settings/sun-poly Admin/isatest/settings/sun-sml Admin/isatest/settings/sun-sml-dev

2010-02-10 blanchet [Wed, 10 Feb 2010 11:47:33 +0100] rev 35087
make Nitpick test a bit weaker;
this should solve failure observed last night on "mac-poly"
src/HOL/Nitpick_Examples/Refute_Nits.thy

2010-02-10 haftmann [Wed, 10 Feb 2010 08:54:56 +0100] rev 35086
merged
src/HOL/Tools/Nitpick/nitpick_model.ML