Changes

Summary

merged
eliminated "xname" and variants;
clarified syntax;
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
tuned;
clarified syntax;
avoid quotes for qualified names;

Changeset 62970:f78cf782bd33 by wenzelm: merged
Changeset 62969:9f394a16c557 by wenzelm: eliminated "xname" and variants;
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Datatypes/Datatypes.thy` (diff)
The file was modified	`src/Doc/Eisbach/Manual.thy` (diff)
The file was modified	`src/Doc/Implementation/Isar.thy` (diff)
The file was modified	`src/Doc/Implementation/Logic.thy` (diff)
The file was modified	`src/Doc/Implementation/ML.thy` (diff)
The file was modified	`src/Doc/Implementation/Prelim.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Document_Preparation.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Generic.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/HOL_Specific.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Inner_Syntax.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Outer_Syntax.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Proof.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Proof_Script.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Spec.thy` (diff)
The file was modified	`src/Doc/JEdit/JEdit.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/ZF_Isar.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/approximation.ML` (diff)
The file was modified	`src/HOL/Library/rewrite.ML` (diff)
The file was modified	`src/HOL/Library/simps_case_conv.ML` (diff)
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_inductive.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_inductive2.ML` (diff)
The file was modified	`src/HOL/SPARK/Manual/Reference.thy` (diff)
The file was modified	`src/HOL/SPARK/Tools/spark_commands.ML` (diff)
The file was modified	`src/HOL/Statespace/state_space.ML` (diff)
The file was modified	`src/HOL/Tools/BNF/bnf_lift.ML` (diff)
The file was modified	`src/HOL/Tools/Function/partial_function.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_def_code_dt.ML` (diff)
The file was modified	`src/HOL/Tools/Lifting/lifting_setup.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/code_prolog.ML` (diff)
The file was modified	`src/HOL/Tools/Predicate_Compile/predicate_compile.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_type.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_util.ML` (diff)
The file was modified	`src/HOL/Tools/inductive.ML` (diff)
The file was modified	`src/HOL/Tools/record.ML` (diff)
The file was modified	`src/HOL/Tools/try0.ML` (diff)
The file was modified	`src/HOL/Tools/value.ML` (diff)
The file was modified	`src/Pure/General/completion.scala` (diff)
The file was modified	`src/Pure/Isar/method.ML` (diff)
The file was modified	`src/Pure/Isar/parse.ML` (diff)
The file was modified	`src/Pure/Isar/parse.scala` (diff)
The file was modified	`src/Pure/Isar/parse_spec.ML` (diff)
The file was modified	`src/Pure/Isar/token.ML` (diff)
The file was modified	`src/Pure/Isar/token.scala` (diff)
The file was modified	`src/Pure/ML/ml_context.ML` (diff)
The file was modified	`src/Pure/PIDE/command.scala` (diff)
The file was modified	`src/Pure/Pure.thy` (diff)
The file was modified	`src/Pure/Thy/sessions.scala` (diff)
The file was modified	`src/Pure/Thy/term_style.ML` (diff)
The file was modified	`src/Pure/Thy/thy_header.ML` (diff)
The file was modified	`src/Pure/Thy/thy_header.scala` (diff)
The file was modified	`src/Pure/Thy/thy_output.ML` (diff)
The file was modified	`src/Pure/Tools/find_consts.ML` (diff)
The file was modified	`src/Pure/Tools/find_theorems.ML` (diff)
The file was modified	`src/Tools/Code/code_target.ML` (diff)
The file was modified	`src/ZF/Tools/datatype_package.ML` (diff)
The file was modified	`src/ZF/Tools/induct_tacs.ML` (diff)
The file was modified	`src/ZF/Tools/inductive_package.ML` (diff)
Changeset 62968:4e4738698db4 by wenzelm: clarified syntax;
The file was modified	`src/Pure/System/options.scala` (diff)
The file was modified	`src/Pure/Thy/sessions.scala` (diff)
Changeset 62967:5e8b1aead28f by wenzelm: more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
The file was modified	`src/Pure/General/name_space.ML` (diff)
Changeset 62966:771b8ad5c7fc by wenzelm: tuned;
The file was modified	`src/Tools/Code/code_ml.ML` (diff)
Changeset 62965:5bf08c9aa036 by wenzelm: clarified syntax;
The file was modified	`src/Doc/Isar_Ref/Document_Preparation.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Spec.thy` (diff)
The file was modified	`src/Pure/Isar/parse.ML` (diff)
The file was modified	`src/Pure/Isar/parse.scala` (diff)
The file was modified	`src/Pure/PIDE/command.scala` (diff)
Changeset 62964:d0c1b2dbca5b by wenzelm: avoid quotes for qualified names;
The file was modified	`src/Pure/General/completion.scala` (diff)