2014-03-21 wenzelm [Fri, 21 Mar 2014 20:33:56 +0100] rev 56245
more qualified names;
NEWS src/CCL/Wfd.thy src/Doc/ProgProve/LaTeXsugar.thy src/FOL/simpdata.ML src/FOLP/hypsubst.ML src/FOLP/simp.ML src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/ferrante_rackoff.ML src/HOL/Decision_Procs/langford.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/Library/LaTeXsugar.thy src/HOL/Library/OptionalSugar.thy src/HOL/Library/refute.ML src/HOL/Matrix_LP/Compute_Oracle/compute.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Refute_Nits.thy src/HOL/Nominal/nominal_primrec.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Product_Type.thy src/HOL/Prolog/prolog.ML src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML src/HOL/TPTP/TPTP_Proof_Reconstruction.thy src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML src/HOL/Tools/Datatype/primrec.ML src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Function/function_common.ML src/HOL/Tools/Function/function_lib.ML src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/smt_utils.ML src/HOL/Tools/SMT/z3_proof_reconstruction.ML src/HOL/Tools/SMT/z3_proof_tools.ML src/HOL/Tools/SMT2/smt2_normalize.ML src/HOL/Tools/SMT2/smt2_util.ML src/HOL/Tools/SMT2/z3_new_proof.ML ...

2014-03-21 wenzelm [Fri, 21 Mar 2014 15:12:03 +0100] rev 56244
more qualified names;
src/HOL/Tools/ATP/atp_problem_generate.ML src/Pure/Proof/proof_rewrite_rules.ML src/Pure/logic.ML src/Pure/pure_thy.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 12:34:50 +0100] rev 56243
more qualified names;
src/Doc/IsarImplementation/Logic.thy src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/Library/Countable.thy src/HOL/Library/refute.ML src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Typerep.thy src/Pure/Proof/proof_syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Syntax/syntax_trans.ML src/Pure/logic.ML src/Pure/primitive_defs.ML src/Pure/pure_thy.ML src/Pure/term.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 12:14:33 +0100] rev 56242
tuned;
src/HOL/Tools/Quickcheck/narrowing_generators.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 11:42:32 +0100] rev 56241
more qualified names;
src/HOL/Code_Evaluation.thy src/HOL/List.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Tools/Ctr_Sugar/case_translation.ML src/HOL/Tools/Quickcheck/exhaustive_generators.ML src/Pure/Proof/proof_syntax.ML src/Pure/Syntax/syntax_phases.ML src/Pure/pure_thy.ML src/Pure/term.ML src/Tools/Code/code_thingol.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 11:06:39 +0100] rev 56240
tuned signature;
src/Doc/Codegen/Setup.thy src/HOL/Imperative_HOL/Overview.thy src/Pure/Isar/isar_syn.ML src/Pure/Proof/proof_syntax.ML src/Pure/pure_thy.ML src/Pure/sign.ML

2014-03-21 wenzelm [Fri, 21 Mar 2014 10:45:03 +0100] rev 56239
tuned signature;
src/Doc/Codegen/Setup.thy src/HOL/HOLCF/Tools/cont_consts.ML src/HOL/Imperative_HOL/Overview.thy src/HOL/Import/import_rule.ML src/HOL/Library/bnf_decl.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/SPARK/Tools/spark_vcs.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/object_logic.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/pure_thy.ML src/Pure/sign.ML src/ZF/Tools/datatype_package.ML

2014-03-21 paulson <lp15@cam.ac.uk> [Fri, 21 Mar 2014 15:36:00 +0000] rev 56238
a few new lemmas and generalisations of old ones
src/HOL/Complex.thy src/HOL/MacLaurin.thy src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy src/HOL/Set_Interval.thy

2014-03-21 traytel [Fri, 21 Mar 2014 08:13:23 +0100] rev 56237
simplified internal datatype construction
src/HOL/BNF_LFP.thy src/HOL/Main.thy src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/BNF/bnf_lfp_tactics.ML src/HOL/Tools/BNF/bnf_lfp_util.ML

2014-03-20 wenzelm [Thu, 20 Mar 2014 23:38:34 +0100] rev 56236
merged