2009-10-29 haftmann [Thu, 29 Oct 2009 11:41:36 +0100] rev 33318
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
src/HOL/Code_Numeral.thy src/HOL/Divides.thy src/HOL/Fun.thy src/HOL/GCD.thy src/HOL/IntDiv.thy src/HOL/IsaMakefile src/HOL/List.thy src/HOL/Nat_Transfer.thy src/HOL/Parity.thy src/HOL/Presburger.thy src/HOL/SetInterval.thy

2009-10-29 wenzelm [Thu, 29 Oct 2009 17:58:26 +0100] rev 33317
standardized filter/filter_out;
src/CCL/Wfd.thy src/FOLP/simp.ML src/HOL/Import/import_syntax.ML src/HOL/Import/shuffler.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_aux.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Datatype/datatype_prop.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/TFL/post.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/meson.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/old_primrec.ML src/HOL/Tools/primrec.ML src/HOL/Tools/refute.ML src/HOL/Tools/sat_solver.ML src/HOL/ex/predicate_compile.ML src/HOLCF/Tools/Domain/domain_axioms.ML src/HOLCF/Tools/Domain/domain_library.ML src/HOLCF/Tools/Domain/domain_theorems.ML src/Provers/Arith/fast_lin_arith.ML src/Provers/classical.ML src/Provers/splitter.ML src/Pure/Isar/rule_insts.ML src/Pure/Proof/extraction.ML src/Pure/Syntax/parser.ML src/Pure/Syntax/syn_ext.ML src/Pure/codegen.ML src/Pure/proofterm.ML src/Pure/unify.ML src/Tools/IsaPlanner/rw_inst.ML src/ZF/arith_data.ML src/ZF/ind_syntax.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:59:12 +0100] rev 33316
modernized some structure names;
src/HOL/ATP_Linkup.thy src/HOL/HOL.thy src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/ATP_Manager/atp_manager.ML src/HOL/Tools/ATP_Manager/atp_minimal.ML src/HOL/Tools/ATP_Manager/atp_wrapper.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML src/HOL/Tools/res_blacklist.ML src/HOL/Tools/res_clause.ML src/HOL/Tools/res_hol_clause.ML src/HOL/Tools/res_reconstruct.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:34:44 +0100] rev 33315
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
src/Pure/Isar/expression.ML src/Pure/axclass.ML src/Pure/more_thm.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:15:33 +0100] rev 33314
modernized functor/structures Interpretation;
src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/typecopy.ML src/HOL/Tools/typedef.ML src/Pure/Isar/code.ML src/Pure/interpretation.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:09:41 +0100] rev 33313
tuned whitespace;
src/HOL/Tools/Datatype/datatype.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:09:16 +0100] rev 33312
unregister: eliminated unused status;
src/HOL/Tools/ATP_Manager/atp_manager.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:08:45 +0100] rev 33311
proper header;
src/HOL/Tools/res_axioms.ML src/HOL/Tools/res_clause.ML src/HOL/Tools/res_hol_clause.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:08:23 +0100] rev 33310
proper header;
tuned whitespace;
src/HOL/Tools/res_reconstruct.ML

2009-10-29 wenzelm [Thu, 29 Oct 2009 16:07:27 +0100] rev 33309
proper header;
adapted ResBlacklist -- eliminated inefficient hash table;
eliminated some old folds;
src/HOL/Tools/res_atp.ML