2015-10-06 wenzelm [Tue, 06 Oct 2015 15:14:28 +0200] rev 61337
fewer aliases for toplevel theorem statements;
NEWS lib/Tools/update_theorems src/CCL/Fix.thy src/CCL/Wfd.thy src/CTT/Arith.thy src/CTT/ex/Elimination.thy src/CTT/ex/Synthesis.thy src/CTT/ex/Typechecking.thy src/Cube/Example.thy src/Doc/Codegen/Evaluation.thy src/Doc/Isar_Ref/Proof.thy src/Doc/Isar_Ref/Spec.thy src/FOL/ex/Classical.thy src/FOL/ex/Prolog.thy src/FOL/ex/Quantifiers_Cla.thy src/FOL/ex/Quantifiers_Int.thy src/FOLP/FOLP.thy src/FOLP/IFOLP.thy src/FOLP/ex/Classical.thy src/FOLP/ex/Foundation.thy src/FOLP/ex/If.thy src/FOLP/ex/Intro.thy src/FOLP/ex/Intuitionistic.thy src/FOLP/ex/Nat.thy src/FOLP/ex/Propositional_Cla.thy src/FOLP/ex/Propositional_Int.thy src/FOLP/ex/Quantifiers_Cla.thy src/FOLP/ex/Quantifiers_Int.thy src/HOL/Bali/Example.thy src/HOL/Eisbach/Tests.thy src/HOL/Groups.thy src/HOL/Hahn_Banach/Vector_Space.thy src/HOL/IMP/Big_Step.thy src/HOL/Inductive.thy src/HOL/Library/Multiset.thy src/HOL/Library/Omega_Words_Fun.thy src/HOL/Library/Prefix_Order.thy src/HOL/Library/Set_Algebras.thy src/HOL/MicroJava/J/Example.thy src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Refute_Nits.thy src/HOL/Prolog/Func.thy src/HOL/Prolog/Test.thy src/HOL/Prolog/Type.thy src/HOL/Proofs/Lambda/LambdaType.thy src/HOL/Wellfounded.thy src/HOL/ex/Classical.thy src/HOL/ex/Groebner_Examples.thy src/HOL/ex/Refute_Examples.thy src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy ...

2015-10-06 wenzelm [Tue, 06 Oct 2015 13:31:44 +0200] rev 61336
just one theorem kind, which is legacy anyway;
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML src/Pure/Isar/expression.ML src/Pure/Isar/isar_syn.ML src/Pure/Tools/thm_deps.ML src/Pure/more_thm.ML src/Tools/permanent_interpretation.ML

2015-10-06 wenzelm [Tue, 06 Oct 2015 11:29:00 +0200] rev 61335
pretty_const: proper local name space;
tuned;
src/Pure/Tools/find_consts.ML

2015-10-06 traytel [Tue, 06 Oct 2015 12:01:07 +0200] rev 61334
collect the names from goals in favor of fragile exports
src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML src/HOL/Tools/BNF/bnf_gfp.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/BNF/bnf_lfp_size.ML src/HOL/Tools/BNF/bnf_lfp_tactics.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2015-10-06 blanchet [Tue, 06 Oct 2015 11:50:23 +0200] rev 61333
compile
src/HOL/Library/Multiset.thy src/HOL/Tools/Nitpick/nitpick_model.ML

2015-10-06 blanchet [Tue, 06 Oct 2015 11:34:07 +0200] rev 61332
tuning
src/HOL/Tools/prop_logic.ML

2015-10-06 blanchet [Tue, 06 Oct 2015 09:27:31 +0200] rev 61331
avoid legacy syntax
src/HOL/Tools/Nitpick/nitpick_model.ML

2015-10-05 blanchet [Mon, 05 Oct 2015 23:03:50 +0200] rev 61330
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
src/HOL/Tools/Sledgehammer/sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

2015-10-05 blanchet [Mon, 05 Oct 2015 21:46:48 +0200] rev 61329
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/ATP/atp_proof.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

2015-10-05 wenzelm [Mon, 05 Oct 2015 18:03:58 +0200] rev 61328
merged