2004-10-12 paulson [Tue, 12 Oct 2004 11:48:21 +0200] rev 15241
tweaks concerned with poly bug-fixing
src/HOL/Hyperreal/Fact.thy src/HOL/Hyperreal/SEQ.thy src/HOL/Hyperreal/Transcendental.thy

2004-10-11 berghofe [Mon, 11 Oct 2004 19:36:48 +0200] rev 15240
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
src/HOL/Integ/presburger.ML src/HOL/Tools/Presburger/presburger.ML

2004-10-11 berghofe [Mon, 11 Oct 2004 16:47:50 +0200] rev 15239
Tuned some proofs.
src/HOL/Integ/Barith.thy

2004-10-11 berghofe [Mon, 11 Oct 2004 10:52:18 +0200] rev 15238
Added entry in Settings menu for Toplevel.skip_proofs flag.
src/Pure/proof_general.ML

2004-10-11 berghofe [Mon, 11 Oct 2004 10:51:19 +0200] rev 15237
Some changes to allow skipping of proof scripts.
src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/toplevel.ML

2004-10-11 nipkow [Mon, 11 Oct 2004 07:42:22 +0200] rev 15236
Proofs needed to be updated because induction now preserves name of
induction variable.
src/HOL/Auth/Guard/Extensions.thy src/HOL/Auth/Guard/Guard.thy src/HOL/Auth/Guard/GuardK.thy src/HOL/HoareParallel/RG_Hoare.thy src/HOL/HoareParallel/RG_Tran.thy src/HOL/Hyperreal/SEQ.thy src/HOL/Lambda/Type.thy src/HOL/Lambda/WeakNorm.thy src/HOL/List.thy src/HOL/Matrix/Float.thy src/HOL/Matrix/MatrixGeneral.thy src/HOL/Matrix/SparseMatrix.thy src/HOL/MicroJava/Comp/CorrComp.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/NumberTheory/Chinese.thy src/HOL/NumberTheory/Factorization.thy src/HOL/NumberTheory/WilsonRuss.thy src/HOL/UNITY/Transformers.thy src/HOL/W0/W0.thy

2004-10-11 nipkow [Mon, 11 Oct 2004 07:39:19 +0200] rev 15235
Induction now preserves the name of the induction variable.
src/Provers/induct_method.ML

2004-10-07 paulson [Thu, 07 Oct 2004 15:42:30 +0200] rev 15234
simplification tweaks for better arithmetic reasoning
src/HOL/Complex/CLim.thy src/HOL/Complex/CStar.thy src/HOL/Complex/Complex.thy src/HOL/Finite_Set.thy src/HOL/Hyperreal/HTranscendental.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/Integration.thy src/HOL/Hyperreal/Lim.thy src/HOL/Hyperreal/MacLaurin.thy src/HOL/Hyperreal/NSA.thy src/HOL/Hyperreal/Series.thy src/HOL/Hyperreal/Transcendental.thy src/HOL/Integ/IntArith.thy src/HOL/Integ/IntDiv.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/NatSimprocs.thy src/HOL/OrderedGroup.thy src/HOL/Real/PReal.thy src/HOL/Real/RComplete.thy src/HOL/Ring_and_Field.thy src/HOL/arith_data.ML

2004-10-06 chaieb [Wed, 06 Oct 2004 13:59:33 +0200] rev 15233
*** empty log message ***
src/HOL/Integ/barith.ML

2004-10-06 chaieb [Wed, 06 Oct 2004 13:58:56 +0200] rev 15232
a very simple decision procedure for a fragment of bounded arithmetic
src/HOL/Integ/Barith.thy src/HOL/Integ/barith.ML