--- a/doc-src/Main/Docs/Main_Doc.thy Wed Mar 28 16:12:17 2012 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Wed Mar 28 17:57:23 2012 +0200
@@ -17,6 +17,11 @@
(Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
end
*}
+setup {*
+ Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single)
+ (fn {source, context, ...} => Thy_Output.output context o
+ Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
+*}
(*>*)
text{*
@@ -264,7 +269,7 @@
\medskip
\noindent
-Type synonym @{typ"'a rel"} @{text"="} @{typ "('a * 'a)set"}
+Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"}
\section{Equiv\_Relations}
--- a/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 28 16:12:17 2012 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 28 17:57:23 2012 +0200
@@ -272,7 +272,7 @@
\medskip
\noindent
-Type synonym \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}
+Type synonym \ \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}
\section{Equiv\_Relations}