2015-04-06 wenzelm [Mon, 06 Apr 2015 23:14:05 +0200] rev 59940
local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;
src/FOL/FOL.thy src/HOL/Extraction.thy src/HOL/HOL.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/Nominal/Nominal.thy src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Tools/inductive.ML src/Tools/induct.ML src/Tools/induction.ML

2015-04-06 wenzelm [Mon, 06 Apr 2015 22:11:01 +0200] rev 59939
support for 'restricted' modifier: only qualified accesses outside the local scope;
NEWS src/Doc/Isar_Ref/Spec.thy src/Pure/General/binding.ML src/Pure/General/name_space.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/outer_syntax.scala src/Pure/Isar/parse.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/token.ML src/Pure/Isar/token.scala src/Pure/Isar/toplevel.ML src/Pure/Pure.thy src/Pure/Thy/thy_output.ML src/Pure/sign.ML src/Tools/jEdit/src/token_markup.scala

2015-04-06 wenzelm [Mon, 06 Apr 2015 17:28:07 +0200] rev 59938
tuned;
src/HOL/SPARK/Manual/Reference.thy

2015-04-06 wenzelm [Mon, 06 Apr 2015 17:20:10 +0200] rev 59937
clarified rail syntax;
src/Doc/Isar_Ref/Document_Preparation.thy src/Pure/Tools/rail.ML

2015-04-06 wenzelm [Mon, 06 Apr 2015 17:06:48 +0200] rev 59936
@{command_spec} is superseded by @{command_keyword};
NEWS src/HOL/Decision_Procs/approximation.ML src/HOL/HOLCF/Tools/Domain/domain.ML src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/cpodef.ML src/HOL/HOLCF/Tools/domaindef.ML src/HOL/HOLCF/Tools/fixrec.ML src/HOL/Import/import_data.ML src/HOL/Import/import_rule.ML src/HOL/Library/Old_SMT/old_smt_config.ML src/HOL/Library/bnf_axiomatization.ML src/HOL/Library/code_test.ML src/HOL/Library/refute.ML src/HOL/Library/simps_case_conv.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Orderings.thy src/HOL/SMT_Examples/boogie.ML src/HOL/SPARK/Tools/spark_commands.ML src/HOL/Statespace/state_space.ML src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.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_compat.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Tools/Ctr_Sugar/case_translation.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/fun_cases.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Function/partial_function.ML src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_info.ML src/HOL/Tools/Lifting/lifting_setup.ML src/HOL/Tools/Nitpick/nitpick_commands.ML src/HOL/Tools/Old_Datatype/old_datatype.ML src/HOL/Tools/Old_Datatype/old_rep_datatype.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Quickcheck/abstract_generators.ML src/HOL/Tools/Quickcheck/find_unused_assms.ML src/HOL/Tools/Quotient/quotient_def.ML src/HOL/Tools/Quotient/quotient_info.ML ...

2015-04-06 wenzelm [Mon, 06 Apr 2015 16:30:44 +0200] rev 59935
clarified command keyword markup;
src/Pure/Isar/isar_syn.ML src/Pure/Isar/keyword.ML src/Pure/Isar/outer_syntax.ML src/Pure/PIDE/markup.ML

2015-04-06 wenzelm [Mon, 06 Apr 2015 16:00:19 +0200] rev 59934
more position information and PIDE markup for command keywords;
src/Pure/Isar/keyword.ML src/Pure/ML/ml_antiquotations.ML src/Pure/PIDE/document.ML src/Pure/PIDE/protocol.ML src/Pure/Thy/thy_header.ML src/Pure/Tools/find_consts.ML src/Pure/Tools/find_theorems.ML

2015-04-06 wenzelm [Mon, 06 Apr 2015 14:09:31 +0200] rev 59933
allow prefix before keyword, notably 'private';
src/Tools/jEdit/src/isabelle_sidekick.scala

2015-04-06 wenzelm [Mon, 06 Apr 2015 13:34:22 +0200] rev 59932
support local command setup;
src/Pure/Isar/outer_syntax.ML

2015-04-06 wenzelm [Mon, 06 Apr 2015 13:28:54 +0200] rev 59931
proper header;
misc tuning;
src/Tools/induction.ML