2014-03-06 wenzelm [Thu, 06 Mar 2014 13:44:01 +0100] rev 55954
more uniform check_const/read_const;
src/Doc/ProgProve/LaTeXsugar.thy src/HOL/Library/LaTeXsugar.thy src/HOL/Tools/Datatype/rep_datatype.ML src/HOL/Tools/Quotient/quotient_info.ML src/HOL/Tools/coinduction.ML src/HOL/Tools/inductive_realizer.ML src/Pure/Isar/args.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML src/Pure/ML/ml_antiquote.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Thy/thy_output.ML src/Tools/adhoc_overloading.ML src/Tools/induct.ML src/Tools/subtyping.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 12:58:51 +0100] rev 55953
tuned;
src/Pure/Syntax/syntax_phases.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 12:43:29 +0100] rev 55952
more rigid type_name demands, based on educated guesses about the tools involved here;
src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Tools/Datatype/datatype_data.ML src/HOL/Tools/Quickcheck/abstract_generators.ML src/HOL/Tools/Quotient/quotient_info.ML src/Pure/Isar/specification.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 12:10:19 +0100] rev 55951
tuned signature -- more uniform check_type_name/read_type_name;
proper reports for read_type_name (lost in 710bc66f432c);
src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Tools/BNF/bnf_lfp_compat.ML src/HOL/Tools/Datatype/datatype_data.ML src/HOL/Tools/Quickcheck/abstract_generators.ML src/HOL/Tools/Quotient/quotient_info.ML src/HOL/Tools/coinduction.ML src/Pure/Isar/args.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/specification.ML src/Pure/ML/ml_antiquote.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Thy/thy_output.ML src/Tools/Code/code_target.ML src/Tools/induct.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 11:32:16 +0100] rev 55950
clarified treatment of consts -- prefer value-oriented reports;
src/Pure/Isar/proof_context.ML src/Pure/Syntax/syntax_phases.ML src/Pure/consts.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 10:53:14 +0100] rev 55949
clarified check of internal names;
src/Pure/Isar/proof_context.ML src/Pure/Syntax/syntax_phases.ML src/Pure/name.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 10:12:47 +0100] rev 55948
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML src/Pure/Isar/proof_context.ML src/Pure/Syntax/syntax_phases.ML src/Pure/Syntax/syntax_trans.ML src/Pure/name.ML src/Pure/variable.ML

2014-03-06 wenzelm [Thu, 06 Mar 2014 10:11:38 +0100] rev 55947
tuned;
src/HOL/Nominal/nominal_induct.ML

2014-03-06 Lars Hupel <lars.hupel@mytum.de> [Thu, 06 Mar 2014 17:55:39 +0100] rev 55946
tuned
src/Pure/Tools/simplifier_trace.ML

2014-03-06 blanchet [Thu, 06 Mar 2014 15:40:33 +0100] rev 55945
renamed 'fun_rel' to 'rel_fun'
NEWS src/Doc/Datatypes/Datatypes.thy src/HOL/BNF_Def.thy src/HOL/BNF_FP_Base.thy src/HOL/BNF_GFP.thy src/HOL/BNF_LFP.thy src/HOL/BNF_Util.thy src/HOL/Basic_BNFs.thy src/HOL/Code_Numeral.thy src/HOL/Int.thy src/HOL/Library/FSet.thy src/HOL/Library/Float.thy src/HOL/Library/Mapping.thy src/HOL/Library/Multiset.thy src/HOL/Library/Quotient_Set.thy src/HOL/Library/Quotient_Syntax.thy src/HOL/Lifting.thy src/HOL/Lifting_Option.thy src/HOL/Lifting_Product.thy src/HOL/Lifting_Set.thy src/HOL/Lifting_Sum.thy src/HOL/List.thy src/HOL/Quotient.thy src/HOL/Quotient_Examples/FSet.thy src/HOL/Real.thy src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_def_tactics.ML src/HOL/Tools/BNF/bnf_fp_util.ML src/HOL/Tools/BNF/bnf_gfp_tactics.ML src/HOL/Tools/BNF/bnf_lfp_tactics.ML src/HOL/Tools/BNF/bnf_util.ML src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_util.ML src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/transfer.ML src/HOL/Topological_Spaces.thy src/HOL/Transfer.thy src/HOL/Word/Word.thy src/HOL/ex/Transfer_Int_Nat.thy