merged

--- a/src/HOL/Analysis/Analysis.thy	Wed Aug 28 23:01:53 2019 +0200
+++ b/src/HOL/Analysis/Analysis.thy	Wed Aug 28 23:19:43 2019 +0200
@@ -43,7 +43,7 @@
   Generalised_Binomial_Theorem
   Gamma_Function
   Change_Of_Vars
-  Lipschitz
+  Multivariate_Analysis
   Simplex_Content
 begin
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Multivariate_Analysis.thy	Wed Aug 28 23:19:43 2019 +0200
@@ -0,0 +1,12 @@
+theory
+  Multivariate_Analysis
+imports
+  Ordered_Euclidean_Space
+  Determinants
+  Cross3
+  Lipschitz
+begin
+
+text \<open>Entry point excluding integration and complex analysis.\<close>
+
+end
\ No newline at end of file

--- a/src/Pure/Isar/expression.ML	Wed Aug 28 23:01:53 2019 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 28 23:19:43 2019 +0200
@@ -396,7 +396,9 @@
         val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
         val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
           handle ERROR msg => if null eqns then error msg else
-            (writeln (msg ^ "\nFalling back to reading rewrites clause first."); ctxt2);
+            (Locale.tracing ctxt1
+             (msg ^ "\nFalling back to reading rewrites clause before activation.");
+             ctxt2);
 
         val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
         val eqns' = (prep_eqns ctxt' o map snd) eqns;

--- a/src/Pure/Isar/locale.ML	Wed Aug 28 23:01:53 2019 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 28 23:19:43 2019 +0200
@@ -96,6 +96,7 @@
     {source: string, target: string, prefix: (string * bool) list, morphism: morphism,
       pos: Position.T, serial: serial}
   val dest_dependencies: theory list -> theory -> locale_dependency list
+  val tracing : Proof.context -> string -> unit
 end;
 
 structure Locale: LOCALE =
@@ -473,11 +474,12 @@
 val trace_locales =
   Attrib.setup_config_bool (Binding.make ("trace_locales", \<^here>)) (K false);
 
+fun tracing context msg =
+  if Config.get context trace_locales then Output.tracing msg else ();
+  
 fun trace kind (name, morph) context =
-  if Config.get_generic context trace_locales
-  then tracing ("Activating " ^ kind ^ " of " ^
-    (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of))
-  else ();
+  tracing (Context.proof_of context) ("Activating " ^ kind ^ " of " ^
+    (pretty_reg (Context.proof_of context) Morphism.identity (name, morph) |> Pretty.string_of));
 
 fun activate_syntax_decls (name, morph) context =
   let