--- 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