# HG changeset patch
# User wenzelm
# Date 1191497194 -7200
# Node ID 137c242e72770b7d2a0d019131fd80b3a220ae53
# Parent  646bdc51eb7deef44d83170f03fda1019161c841
updated Sign.add_abbrev;

diff -r 646bdc51eb7d -r 137c242e7277 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Oct 04 12:32:58 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Oct 04 13:26:34 2007 +0200
@@ -329,7 +329,7 @@
   \indexml{lambda}\verb|lambda: term -> term -> term| \\
   \indexml{betapply}\verb|betapply: term * term -> term| \\
   \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
-  \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> bstring * term -> theory -> (term * term) * theory| \\
+  \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory| \\
   \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
   \end{mldecls}
@@ -369,7 +369,7 @@
   \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
   new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
 
-  \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
+  \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
   introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
 
   \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
diff -r 646bdc51eb7d -r 137c242e7277 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 04 12:32:58 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 04 13:26:34 2007 +0200
@@ -327,7 +327,7 @@
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> bstring * term -> theory -> (term * term) * theory"} \\
+  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory"} \\
   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   \end{mldecls}
@@ -375,7 +375,7 @@
   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
 
-  \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
+  \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
   introduces a new term abbreviation @{text "c \<equiv> t"}.
 
   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML