2010-02-08 haftmann [Mon, 08 Feb 2010 11:13:30 +0100] rev 35030
merged
NEWS src/HOL/Tools/numeral_simprocs.ML

2010-02-08 haftmann [Mon, 08 Feb 2010 10:36:02 +0100] rev 35029
separate theory for index structures
NEWS src/HOL/IsaMakefile src/HOL/Library/Library.thy src/HOL/Library/Structure_Syntax.thy

2010-02-05 haftmann [Fri, 05 Feb 2010 14:33:50 +0100] rev 35028
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
src/HOL/Archimedean_Field.thy src/HOL/Code_Numeral.thy src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Decision_Procs/Polynomial_List.thy src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy src/HOL/Fact.thy src/HOL/Finite_Set.thy src/HOL/GCD.thy src/HOL/Import/HOL/real.imp src/HOL/Int.thy src/HOL/Lattices.thy src/HOL/Library/Abstract_Rat.thy src/HOL/Library/BigO.thy src/HOL/Library/Kleene_Algebra.thy src/HOL/Library/Multiset.thy src/HOL/Library/Nat_Infinity.thy src/HOL/Library/Polynomial.thy src/HOL/Library/Univ_Poly.thy src/HOL/Library/positivstellensatz.ML src/HOL/List.thy src/HOL/Matrix/ComputeNumeral.thy src/HOL/Matrix/LP.thy src/HOL/Matrix/Matrix.thy src/HOL/Matrix/SparseMatrix.thy src/HOL/Matrix/cplex/Cplex.thy src/HOL/Metis_Examples/BigO.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Determinants.thy src/HOL/Multivariate_Analysis/Euclidean_Space.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/HyperNat.thy src/HOL/NSA/StarDef.thy src/HOL/Nat.thy src/HOL/Nat_Numeral.thy src/HOL/Nitpick.thy src/HOL/OrderedGroup.thy src/HOL/Orderings.thy src/HOL/PReal.thy src/HOL/Parity.thy src/HOL/Power.thy src/HOL/Probability/Borel.thy src/HOL/Quickcheck.thy src/HOL/RComplete.thy src/HOL/Rational.thy src/HOL/Real.thy src/HOL/RealDef.thy ...

2010-02-05 haftmann [Fri, 05 Feb 2010 14:33:31 +0100] rev 35027
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
NEWS

2010-02-05 haftmann [Fri, 05 Feb 2010 14:33:29 +0100] rev 35026
added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration
src/HOL/Algebras.thy

2010-02-08 boehmes [Mon, 08 Feb 2010 11:01:47 +0100] rev 35025
split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts,
modernized perl scripts: prefer standalone executables
src/HOL/SMT/Tools/smt_solver.ML src/HOL/SMT/etc/settings src/HOL/SMT/lib/scripts/remote_smt src/HOL/SMT/lib/scripts/run_smt_solver src/HOL/SMT/lib/scripts/run_smt_solver.pl

2010-02-07 wenzelm [Sun, 07 Feb 2010 20:44:25 +0100] rev 35024
removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);
lib/scripts/bash

2010-02-07 wenzelm [Sun, 07 Feb 2010 20:21:38 +0100] rev 35023
modernized perl scripts: prefer standalone executables;
exec bash wrapper script directly -- avoid intermediate process;
lib/scripts/bash lib/scripts/system.pl src/Pure/ML-Systems/bash.ML src/Pure/ML-Systems/multithreading_polyml.ML src/Pure/System/isabelle_system.scala

2010-02-07 wenzelm [Sun, 07 Feb 2010 19:54:12 +0100] rev 35022
modernized perl scripts: prefer standalone executables;
lib/Tools/keywords lib/Tools/unsymbolize lib/Tools/yxml lib/scripts/keywords lib/scripts/keywords.pl lib/scripts/unsymbolize lib/scripts/unsymbolize.pl lib/scripts/yxml lib/scripts/yxml.pl

2010-02-07 wenzelm [Sun, 07 Feb 2010 19:33:34 +0100] rev 35021
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
NEWS src/FOL/simpdata.ML src/FOLP/simp.ML src/HOL/Import/hol4rews.ML src/HOL/Import/shuffler.ML src/HOL/Matrix/cplex/matrixlp.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Statespace/state_fun.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/TFL/post.ML src/HOL/Tools/arith_data.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/record.ML src/HOL/Tools/split_rule.ML src/HOL/Tools/typedef.ML src/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOLCF/Tools/Domain/domain_theorems.ML src/HOLCF/Tools/pcpodef.ML src/HOLCF/Tools/repdef.ML src/Provers/hypsubst.ML src/Provers/typedsimp.ML src/Pure/Isar/attrib.ML src/Pure/Isar/class.ML src/Pure/Isar/class_target.ML src/Pure/Isar/expression.ML src/Pure/Isar/skip_proof.ML src/Pure/ML/ml_context.ML src/Pure/axclass.ML src/Pure/drule.ML src/Pure/goal.ML src/Pure/old_goals.ML src/Sequents/simpdata.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/inductive_package.ML src/ZF/ind_syntax.ML