2010-01-22 haftmann [Fri, 22 Jan 2010 16:56:51 +0100] rev 34962
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
NEWS src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/hologic.ML src/HOL/Tools/inductive_codegen.ML

2010-01-22 boehmes [Fri, 22 Jan 2010 16:38:58 +0100] rev 34961
merged

2010-01-22 boehmes [Fri, 22 Jan 2010 16:38:21 +0100] rev 34960
support skolem constant for extensional arrays in Z3 proofs
src/HOL/SMT/SMT_Base.thy src/HOL/SMT/Tools/z3_proof.ML src/HOL/SMT/Tools/z3_proof_rules.ML src/HOL/SMT/Tools/z3_proof_terms.ML

2010-01-22 boehmes [Fri, 22 Jan 2010 16:33:44 +0100] rev 34959
drop underscores at end of names coming from Boogie
src/HOL/Boogie/Tools/boogie_loader.ML

2010-01-22 bulwahn [Fri, 22 Jan 2010 15:26:29 +0100] rev 34958
merged
src/HOL/IsaMakefile

2010-01-22 bulwahn [Fri, 22 Jan 2010 11:42:28 +0100] rev 34957
correctly hiding facts of Lazy_Sequence
src/HOL/Lazy_Sequence.thy

2010-01-21 bulwahn [Thu, 21 Jan 2010 14:13:21 +0100] rev 34956
corrected and simplified Spec_Rules registration in the Recdef package
src/HOL/Tools/recdef.ML

2010-01-21 bulwahn [Thu, 21 Jan 2010 12:20:28 +0100] rev 34955
merged

2010-01-21 bulwahn [Thu, 21 Jan 2010 12:18:41 +0100] rev 34954
adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

2010-01-20 bulwahn [Wed, 20 Jan 2010 18:08:08 +0100] rev 34953
adopting Sequences
src/HOL/DSequence.thy src/HOL/Random_Sequence.thy