proper name space "kind": this is a formal name, not comment;
authorwenzelm
Tue, 03 Aug 2021 13:40:17 +0200
changeset 74113 228adc502803
parent 74112 d0527bb2e590
child 74114 700e5bd59c7d
proper name space "kind": this is a formal name, not comment;
src/HOL/Real_Asymp/exp_log_expression.ML
src/HOL/Real_Asymp/multiseries_expansion.ML
--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Tue Aug 03 13:08:23 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Tue Aug 03 13:40:17 2021 +0200
@@ -128,7 +128,7 @@
   fun eq_entry ({name = name1, ...}, {name = name2, ...}) = (name1 = name2)
   val empty = 
     {
-      name_table = Name_Space.empty_table "Exp-Log Custom Function",
+      name_table = Name_Space.empty_table "exp_log_custom_function",
       net = Item_Net.init eq_entry (fn {net_pat, ...} => [net_pat])
     }
   
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML	Tue Aug 03 13:08:23 2021 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML	Tue Aug 03 13:40:17 2021 +0200
@@ -135,7 +135,7 @@
 structure Data = Generic_Data
 (
   type T = (Proof.context -> int -> tactic) Name_Space.table;
-  val empty : T = Name_Space.empty_table "sign oracle tactics";
+  val empty : T = Name_Space.empty_table "sign_oracle_tactic";
   val extend = I;
   fun merge (tactics1, tactics2) : T = Name_Space.merge_tables (tactics1, tactics2);
 );