2007-06-14 wenzelm [Thu, 14 Jun 2007 23:04:39 +0200] rev 23394
tuned proofs;
src/HOL/Library/Char_nat.thy src/HOL/Library/Char_ord.thy src/HOL/Library/EfficientNat.thy src/HOL/Library/ExecutableSet.thy src/HOL/Library/Graphs.thy src/HOL/Library/Infinite_Set.thy src/HOL/Library/Kleene_Algebras.thy src/HOL/Library/List_Prefix.thy src/HOL/Library/NatPair.thy src/HOL/Library/Nested_Environment.thy src/HOL/Library/Quotient.thy src/HOL/Library/SCT_Implementation.thy src/HOL/Library/SCT_Interpretation.thy src/HOL/Library/SCT_Misc.thy src/HOL/Library/SCT_Theorem.thy src/HOL/Unix/Unix.thy

2007-06-14 wenzelm [Thu, 14 Jun 2007 23:04:36 +0200] rev 23393
tuned proofs: avoid implicit prems;
src/FOL/IFOL.thy src/HOL/Isar_examples/BasicLogic.thy src/HOL/Lattice/Bounds.thy src/HOL/Lattice/Lattice.thy src/HOL/Nominal/Examples/CR.thy src/HOL/Nominal/Examples/Class.thy src/HOL/Nominal/Examples/Crary.thy src/HOL/Nominal/Examples/Fsub.thy src/HOL/Nominal/Examples/Height.thy src/HOL/Nominal/Examples/SN.thy src/HOL/Nominal/Examples/SOS.thy src/HOL/Nominal/Nominal.thy

2007-06-14 chaieb [Thu, 14 Jun 2007 22:59:42 +0200] rev 23392
fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
src/HOL/Tools/Presburger/presburger.ML

2007-06-14 chaieb [Thu, 14 Jun 2007 22:59:40 +0200] rev 23391
no computation rules in the pre-simplifiaction set
src/HOL/Tools/Presburger/cooper_data.ML

2007-06-14 chaieb [Thu, 14 Jun 2007 22:59:39 +0200] rev 23390
Added some lemmas to default presburger simpset; tuned proofs
src/HOL/Presburger.thy

2007-06-14 wenzelm [Thu, 14 Jun 2007 18:33:31 +0200] rev 23389
tuned proofs: avoid implicit prems;
src/HOL/Finite_Set.thy src/HOL/Groebner_Basis.thy src/HOL/HOL.thy src/HOL/Import/HOL4Compat.thy src/HOL/Inductive.thy src/HOL/Lattices.thy src/HOL/Library/SCT_Theorem.thy src/HOL/NatBin.thy src/HOL/Numeral.thy src/HOL/OrderedGroup.thy src/HOL/Predicate.thy src/HOL/Presburger.thy src/HOL/Real/ContNotDenum.thy src/HOL/Real/PReal.thy src/HOL/Real/RComplete.thy src/HOL/Ring_and_Field.thy src/HOL/Wellfounded_Recursion.thy src/HOL/ex/CTL.thy

2007-06-14 wenzelm [Thu, 14 Jun 2007 18:33:29 +0200] rev 23388
tuned proofs: avoid implicit prems;
tuned partition proofs;
src/HOL/List.thy

2007-06-14 paulson [Thu, 14 Jun 2007 13:19:50 +0200] rev 23387
Now ResHolClause also does first-order problems!
src/HOL/Tools/res_atp.ML

2007-06-14 paulson [Thu, 14 Jun 2007 13:18:59 +0200] rev 23386
Now also handles FO problems
src/HOL/Tools/res_hol_clause.ML

2007-06-14 paulson [Thu, 14 Jun 2007 13:18:24 +0200] rev 23385
Deleted unused code
src/HOL/Tools/res_clause.ML