--- a/doc-src/Classes/Thy/Classes.thy Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Wed Aug 11 12:04:49 2010 +0200
@@ -611,13 +611,12 @@
text {*
\noindent This maps to Haskell as follows:
*}
-
+(*<*)code_include %invisible Haskell "Natural" -(*>*)
text %quote {*@{code_stmts example (Haskell)}*}
text {*
\noindent The code in SML has explicit dictionary passing:
*}
-
text %quote {*@{code_stmts example (SML)}*}
subsection {* Inspecting the type class universe *}
--- a/doc-src/Classes/Thy/Setup.thy Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Classes/Thy/Setup.thy Wed Aug 11 12:04:49 2010 +0200
@@ -1,8 +1,8 @@
theory Setup
imports Main Code_Integer
uses
- "../../antiquote_setup"
- "../../more_antiquote"
+ "../../antiquote_setup.ML"
+ "../../more_antiquote.ML"
begin
setup {* Code_Target.set_default_code_width 74 *}
--- a/doc-src/Classes/Thy/document/Classes.tex Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Aug 11 12:04:49 2010 +0200
@@ -1132,6 +1132,19 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
\isadelimquote
%
\endisadelimquote
--- a/doc-src/Main/Docs/Main_Doc.thy Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Wed Aug 11 12:04:49 2010 +0200
@@ -109,7 +109,7 @@
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
@{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
-@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
+@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
--- a/doc-src/TutorialI/Fun/ROOT.ML Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Fun/ROOT.ML Wed Aug 11 12:04:49 2010 +0200
@@ -1,2 +1,2 @@
-use "../settings";
+use "../settings.ML";
use_thy "fun0";
--- a/doc-src/TutorialI/Types/Axioms.thy Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy Wed Aug 11 12:04:49 2010 +0200
@@ -59,7 +59,7 @@
text {* \noindent Again, the interesting things enter the stage with
parametric types: *}
-instantiation * :: (semigroup, semigroup) semigroup
+instantiation prod :: (semigroup, semigroup) semigroup
begin
instance proof
@@ -112,7 +112,7 @@
This covers products as well:
*}
-instantiation * :: (monoidl, monoidl) monoidl
+instantiation prod :: (monoidl, monoidl) monoidl
begin
definition
--- a/doc-src/TutorialI/Types/Overloading.thy Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Wed Aug 11 12:04:49 2010 +0200
@@ -55,10 +55,10 @@
text {* \noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
legal. *}
-instantiation "*" :: (plus, plus) plus
+instantiation prod :: (plus, plus) plus
begin
-text {* \noindent Here we instantiate the product type @{type "*"} to
+text {* \noindent Here we instantiate the product type @{type prod} to
class @{class [source] plus}, given that its type arguments are of
class @{class [source] plus}: *}
--- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Aug 11 12:04:49 2010 +0200
@@ -123,7 +123,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
@@ -226,7 +226,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
--- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Aug 11 12:04:49 2010 +0200
@@ -99,10 +99,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instantiation}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
\isakeyword{begin}%
\begin{isamarkuptext}%
-\noindent Here we instantiate the product type \isa{{\isacharasterisk}} to
+\noindent Here we instantiate the product type \isa{prod} to
class \isa{plus}, given that its type arguments are of
class \isa{plus}:%
\end{isamarkuptext}%