2009-06-24 nipkow [Wed, 24 Jun 2009 09:41:14 +0200] rev 31790
corrected and unified thm names
NEWS src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/Groebner_Basis.thy src/HOL/Import/HOL/arithmetic.imp src/HOL/Library/Formal_Power_Series.thy src/HOL/MetisExamples/BT.thy src/HOL/Nat_Numeral.thy src/HOL/Presburger.thy src/HOL/Tools/Groebner_Basis/normalizer.ML src/HOL/Tools/Qelim/presburger.ML src/HOL/Tools/nat_numeral_simprocs.ML src/HOL/Transcendental.thy src/HOL/Word/BinBoolList.thy

2009-06-23 haftmann [Tue, 23 Jun 2009 21:07:39 +0200] rev 31789
merged

2009-06-23 haftmann [Tue, 23 Jun 2009 21:05:59 +0200] rev 31788
merged

2009-06-23 haftmann [Tue, 23 Jun 2009 21:03:31 +0200] rev 31787
Datatype.get_all
src/HOLCF/IOA/Modelcheck/MuIOA.thy

2009-06-23 haftmann [Tue, 23 Jun 2009 18:10:39 +0200] rev 31786
corrected handling of free variables in arguments
src/HOL/Tools/primrec.ML

2009-06-23 haftmann [Tue, 23 Jun 2009 17:17:07 +0200] rev 31785
tuned proof
src/HOL/Tools/quickcheck_generators.ML

2009-06-23 haftmann [Tue, 23 Jun 2009 16:27:12 +0200] rev 31784
tuned interfaces of datatype module
NEWS src/HOL/Inductive.thy src/HOL/List.thy src/HOL/Nominal/nominal.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Statespace/state_fun.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Function/fundef.ML src/HOL/Tools/Function/fundef_datatype.ML src/HOL/Tools/Function/pattern_split.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/TFL/casesplit.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/TFL/thry.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/old_primrec.ML src/HOL/Tools/primrec.ML src/HOL/Tools/quickcheck_generators.ML src/HOL/Tools/refute.ML src/HOL/ex/predicate_compile.ML

2009-06-23 haftmann [Tue, 23 Jun 2009 15:32:34 +0200] rev 31783
add_datatypes does not yield particular rules any longer
src/HOL/Nominal/nominal.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/inductive_realizer.ML

2009-06-23 haftmann [Tue, 23 Jun 2009 14:51:21 +0200] rev 31782
merged

2009-06-23 haftmann [Tue, 23 Jun 2009 14:50:34 +0200] rev 31781
add_datatype interface yields type names and less rules
src/HOL/Nominal/nominal.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/inductive_realizer.ML