Merge pull request #500 from binghe/relationTheory.INV

Added TeX notation for relation inversion (relinv)
HOL-Theorem-Prover · Dec 1, 2017 · a7de884 · a7de884
2 parents ffc6d5e + ba8a228
commit a7de884
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/src/TeX/holtexbasic.sty b/src/TeX/holtexbasic.sty
@@ -111,6 +111,7 @@
 \newcommand{\HOLTokenCompose}{\ensuremath{\circ}}
 \newcommand{\HOLTokenRCompose}{\ensuremath{\circ_r}}
 \newcommand{\HOLTokenInverse}{\ensuremath{{}^{-1}}}
+\newcommand{\HOLTokenRInverse}{\ensuremath{{}^T}}
 \newcommand{\HOLTokenHilbert}{\ensuremath{\varepsilon}}
 \newcommand{\HOLTokenBagLeft}{\ensuremath{\{\!|}}
 \newcommand{\HOLTokenBagRight}{\ensuremath{|\!\}}}

diff --git a/src/relation/relationScript.sml b/src/relation/relationScript.sml
@@ -1596,6 +1596,8 @@ val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
                    pp_elements = [TOK (UTF8.chr 0x1D40)],
                    term_name = "relinv"}
 val _ = overload_on("relinv", ``inv``)
+val _ = TeX_notation { hol = (UTF8.chr 0x1D40),
+                       TeX = ("\\HOLTokenRInverse{}", 1) }
 
 val inv_inv = store_thm(
   "inv_inv",