# HG changeset patch
# User wenzelm
# Date 1538304057 -7200
# Node ID 1b656a2ec0adbd42707555ec92095e2d65ff2aba
# Parent  43dade957d59ef8f7c37f05eb3fe5241b1a45e7a
tuned spelling;

diff -r 43dade957d59 -r 1b656a2ec0ad src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Sun Sep 30 12:36:31 2018 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Sun Sep 30 12:40:57 2018 +0200
@@ -385,7 +385,7 @@
     val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
       dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule
     val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name
-      then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
+      then error ("Monotonicity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
       else ()
     val neg_mono_rule = negate_mono_rule pol_mono_rule
     val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule,
@@ -405,12 +405,12 @@
       if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then
         Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)))
           ctxt
-      else error "The monoticity rule is not defined."
+      else error "The monotonicity rule is not defined."
     end
 
-    fun rewrite_concl_conv thm ctm =
-      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
-      handle CTERM _ => error "The rule has a wrong format."
+  fun rewrite_concl_conv thm ctm =
+    Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
+    handle CTERM _ => error "The rule has a wrong format."
 
 in
   fun add_pos_distr_rule distr_rule ctxt =
@@ -513,7 +513,7 @@
 val _ =
   Theory.setup
     (Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
-      "declaration of relator's monoticity"
+      "declaration of relator's monotonicity"
     #> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))
       "declaration of relator's distributivity over OO"
     #> Global_Theory.add_thms_dynamic