2009-11-13 wenzelm [Fri, 13 Nov 2009 19:57:46 +0100] rev 33669
inductive: eliminated obsolete kind;
src/HOL/Nominal/nominal_datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_rep_proofs.ML src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/inductive_set.ML

2009-11-13 paulson [Fri, 13 Nov 2009 17:15:35 +0000] rev 33668
merged

2009-11-13 paulson [Fri, 13 Nov 2009 17:15:12 +0000] rev 33667
A little rationalisation
src/HOL/Ln.thy src/HOL/Transcendental.thy

2009-11-13 wenzelm [Fri, 13 Nov 2009 17:25:09 +0100] rev 33666
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/primrec.ML src/HOL/Tools/quickcheck_generators.ML src/HOLCF/Tools/fixrec.ML src/Pure/Isar/attrib.ML src/Pure/more_thm.ML

2009-11-13 boehmes [Fri, 13 Nov 2009 15:48:52 +0100] rev 33665
merged

2009-11-13 boehmes [Fri, 13 Nov 2009 15:47:37 +0100] rev 33664
removed unused code and unused arguments,
tuned
src/HOL/SMT/Tools/cvc3_solver.ML src/HOL/SMT/Tools/smt_normalize.ML src/HOL/SMT/Tools/smt_solver.ML src/HOL/SMT/Tools/smt_translate.ML src/HOL/SMT/Tools/yices_solver.ML src/HOL/SMT/Tools/z3_model.ML src/HOL/SMT/Tools/z3_proof_rules.ML src/HOL/SMT/Tools/z3_proof_terms.ML

2009-11-13 boehmes [Fri, 13 Nov 2009 15:11:41 +0100] rev 33663
adapted proofs due to changes in HOL-Boogie
src/HOL/Boogie/Examples/Boogie_Max.thy src/HOL/Boogie/Examples/cert/Boogie_Dijkstra src/HOL/Boogie/Examples/cert/Boogie_Dijkstra.proof src/HOL/Boogie/Examples/cert/Boogie_max src/HOL/Boogie/Examples/cert/Boogie_max.proof src/HOL/Boogie/Examples/cert/VCC_maximum src/HOL/Boogie/Examples/cert/VCC_maximum.proof

2009-11-13 boehmes [Fri, 13 Nov 2009 15:10:28 +0100] rev 33662
parallel solving of Boogie splinters
src/HOL/Boogie/Tools/boogie_split.ML

2009-11-13 boehmes [Fri, 13 Nov 2009 15:06:19 +0100] rev 33661
corrected translation of integer operators,
keep argument order for n-ary symbols (conjunction, disjunction),
removed unused code
src/HOL/Boogie/Tools/boogie_loader.ML

2009-11-13 boehmes [Fri, 13 Nov 2009 15:02:51 +0100] rev 33660
extended theory simpset to simplify non-linear problems
src/HOL/SMT/Tools/z3_proof_rules.ML